1.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
1.2 +++ b/src/Tools/isac/Knowledge/Partial_Fractions.thy Fri Sep 23 16:22:11 2011 +0200
1.3 @@ -0,0 +1,32 @@
1.4 +theory Partial_Fractions imports Rational begin
1.5 +
1.6 +subsection {*get the denominator out of a fraction*}
1.7 +text {*this function can be put into rule sets*}
1.8 +ML {*
1.9 +(*("get_denominator", ("Rational.get'_denominator", eval_get_denominator ""))*)
1.10 +fun eval_get_denominator (thmid:string) _
1.11 + (t as (Const("Rings.inverse_class.divide", _) $ num $ denom)) thy =
1.12 + SOME (mk_thmid thmid ""
1.13 + (Print_Mode.setmp [] (Syntax.string_of_term (thy2ctxt thy)) denom) "",
1.14 + Trueprop $ (mk_equality (t, denom)))
1.15 + | eval_get_denominator _ _ _ _ = NONE;
1.16 +*}
1.17 +text {*rule set for partial fractions*}
1.18 +ML {*
1.19 +val partial_fraction =
1.20 + Rls {id="partial_fraction", preconds = [], rew_ord = ("termlessI",termlessI),
1.21 + erls = Erls, srls = Erls, calc = [],
1.22 + rules = [
1.23 + Calc ("Rings.inverse_class.divide", eval_get_denominator "#")
1.24 + ],
1.25 + scr = EmptyScr};
1.26 +*}
1.27 +text {*store the rule set for math engine*}
1.28 +ML {*
1.29 + overwritelthy @{theory} (!ruleset',
1.30 + [("partial_fraction", prep_rls partial_fraction)
1.31 + ]);
1.32 +*}
1.33 +
1.34 +
1.35 +end
1.36 \ No newline at end of file
2.1 --- a/test/Tools/isac/ADDTESTS/course/SignalProcess/Build_Inverse_Z_Transform.thy Fri Sep 23 14:56:14 2011 +0200
2.2 +++ b/test/Tools/isac/ADDTESTS/course/SignalProcess/Build_Inverse_Z_Transform.thy Fri Sep 23 16:22:11 2011 +0200
2.3 @@ -5,9 +5,12 @@
2.4 10 20 30 40 50 60 70 80
2.5 *)
2.6
2.7 -theory Build_Inverse_Z_Transform imports Isac begin
2.8 +theory Build_Inverse_Z_Transform imports
2.9 + Isac "../../../../../../src/Tools/isac/Knowledge/Partial_Fractions"
2.10 +
2.11 +begin
2.12
2.13 -text{*We stepwise build Inverse_Z_Transform.thy as an exercise.
2.14 +text{* We stepwise build Inverse_Z_Transform.thy as an exercise.
2.15 Because subsection "Stepwise Check the Program" requires Inverse_Z_Transform.thy
2.16 as a subtheory of Isac.thy, the setup has been changed from
2.17 "theory Inverse_Z_Transform imports Isac begin.." to the above.
2.18 @@ -115,9 +118,23 @@
2.19 term2str fun3; (*fails on x^^^(-1) TODO*)
2.20 val SOME (fun3',_) = rewrite_set_ @{theory Isac} false norm_Rational fun2';
2.21 term2str fun3'; (*OK*)
2.22 +*}
2.23
2.24 +subsection {*build equation from given term*}
2.25 +ML {*
2.26 val (_, expr) = HOLogic.dest_eq fun3'; term2str expr;
2.27 +val (_, denom) = HOLogic.dest_bin "Rings.inverse_class.divide" (type_of expr) expr;
2.28 +term2str denom = "-1 + -2 * z + 8 * z ^^^ 2";
2.29 *}
2.30 +text {*we have rhs in the language, but we need a function
2.31 + which gets the denominator of a fraction*}
2.32 +ML {*
2.33 +(*GOON ==========================================================================================*)
2.34 +
2.35 +*}
2.36 +ML {*
2.37 +*}
2.38 +ML {**}
2.39
2.40 subsection {*solve equation*}
2.41 text {*this type of equation if too general for the present program*}
2.42 @@ -483,8 +500,8 @@
2.43 ],
2.44 {rew_ord'="tless_true", rls'= e_rls, calc = [], srls = e_rls, prls = e_rls,
2.45 crls = e_rls, nrls = e_rls},
2.46 -"Script InverseZTransform (Xeq::bool) =" ^ (*(1/z) instead of z ^^^ -1*)
2.47 -" (let X = Take Xeq;" ^
2.48 +"Script InverseZTransform (X_eq::bool) =" ^ (*(1/z) instead of z ^^^ -1*)
2.49 +" (let X = Take X_eq;" ^
2.50 " X' = Rewrite ruleZY False X;" ^ (*z * denominator*)
2.51 " X' = (Rewrite_Set norm_Rational False) X';" ^ (*simplify*)
2.52 " funterm = rhs X'" ^ (*drop X'= for equation solving*)
2.53 @@ -511,9 +528,6 @@
2.54
2.55 subsubsection {*Stepwise check the program*}
2.56 ML {*
2.57 -"----------- Apply_Method: exception PTREE get_obj: pos = [0] does";
2.58 -"----------- Apply_Method: exception PTREE get_obj: pos = [0] does";
2.59 -"----------- Apply_Method: exception PTREE get_obj: pos = [0] does";
2.60 val fmz = ["filterExpression (X z = 3 / (z - 1/4 + -1/8 * (1/(z::real))))",
2.61 "stepResponse (x[n::real]::bool)"];
2.62 val (dI,pI,mI) = ("Isac", ["inverse", "Z_Transform", "SignalProcessing"],
2.63 @@ -524,21 +538,19 @@
2.64 val (p,_,fb,nxt,_,pt) = me nxt p [] pt;
2.65 val (p,_,fb,nxt,_,pt) = me nxt p [] pt;
2.66 val (p,_,fb,nxt,_,pt) = me nxt p [] pt;
2.67 +val (p,_,fb,nxt,_,pt) = me nxt p [] pt;
2.68 +val (p,_,fb,nxt,_,pt) = me nxt p [] pt;
2.69 +val (p,_,fb,nxt,_,pt) = me nxt p [] pt;
2.70 +val (p,_,fb,nxt,_,pt) = me nxt p [] pt;
2.71 *}
2.72 ML {*
2.73 val (p,_,fb,nxt,_,pt) = me nxt p [] pt;
2.74 *}
2.75 ML {*
2.76 +show_pt pt;
2.77 *}
2.78 ML {*
2.79 -(*
2.80 -val (p,_,fb,nxt,_,pt) = me nxt p [] pt;
2.81 -exception PTREE "get_obj: pos = [0] does not exist"
2.82 -raised (line 908 of "/usr/local/isabisac/src/Tools/isac/Interpret/ctree.sml")
2.83 -*)
2.84 *}
2.85 -
2.86 -
2.87 ML {*
2.88
2.89 *}
2.90 @@ -560,13 +572,10 @@
2.91 *}
2.92
2.93 ML {*
2.94 -
2.95 *}
2.96 ML {*
2.97 -
2.98 *}
2.99 ML {*
2.100 -
2.101 *}
2.102
2.103
3.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
3.2 +++ b/test/Tools/isac/ADDTESTS/course/SignalProcess/document/Build_Inverse_Z_Transform.tex Fri Sep 23 16:22:11 2011 +0200
3.3 @@ -0,0 +1,1275 @@
3.4 +%
3.5 +\begin{isabellebody}%
3.6 +\def\isabellecontext{Build{\isaliteral{5F}{\isacharunderscore}}Inverse{\isaliteral{5F}{\isacharunderscore}}Z{\isaliteral{5F}{\isacharunderscore}}Transform}%
3.7 +%
3.8 +\isadelimtheory
3.9 +\isanewline
3.10 +\isanewline
3.11 +%
3.12 +\endisadelimtheory
3.13 +%
3.14 +\isatagtheory
3.15 +\isacommand{theory}\isamarkupfalse%
3.16 +\ Build{\isaliteral{5F}{\isacharunderscore}}Inverse{\isaliteral{5F}{\isacharunderscore}}Z{\isaliteral{5F}{\isacharunderscore}}Transform\ \isakeyword{imports}\ Isac\ \isakeyword{begin}%
3.17 +\endisatagtheory
3.18 +{\isafoldtheory}%
3.19 +%
3.20 +\isadelimtheory
3.21 +%
3.22 +\endisadelimtheory
3.23 +%
3.24 +\begin{isamarkuptext}%
3.25 +We stepwise build Inverse_Z_Transform.thy as an exercise.
3.26 + Because subsection "Stepwise Check the Program" requires Inverse_Z_Transform.thy
3.27 + as a subtheory of Isac.thy, the setup has been changed from
3.28 + "theory Inverse_Z_Transform imports Isac begin.." to the above.
3.29 +
3.30 + ATTENTION WITH NAMES OF IDENTIFIERS WHEN GOING INTO INTERNALS:
3.31 + Here in this theory there are the internal names twice, for instance we have
3.32 + (Thm.derivation_name \isa{rule{\isadigit{1}}} = "Build_Inverse_Z_Transform.rule1") = true;
3.33 + but actually in us will be "Inverse_Z_Transform.rule1"%
3.34 +\end{isamarkuptext}%
3.35 +\isamarkuptrue%
3.36 +%
3.37 +\isadelimML
3.38 +%
3.39 +\endisadelimML
3.40 +%
3.41 +\isatagML
3.42 +\isacommand{ML}\isamarkupfalse%
3.43 +\ {\isaliteral{7B2A}{\isacharverbatimopen}}val\ thy\ {\isaliteral{3D}{\isacharequal}}\ %
3.44 +\isaantiq
3.45 +theory\ Isac{}%
3.46 +\endisaantiq
3.47 +{\isaliteral{3B}{\isacharsemicolon}}{\isaliteral{2A7D}{\isacharverbatimclose}}%
3.48 +\endisatagML
3.49 +{\isafoldML}%
3.50 +%
3.51 +\isadelimML
3.52 +%
3.53 +\endisadelimML
3.54 +%
3.55 +\isamarkupsection{trials towards Z transform%
3.56 +}
3.57 +\isamarkuptrue%
3.58 +%
3.59 +\begin{isamarkuptext}%
3.60 +===============================%
3.61 +\end{isamarkuptext}%
3.62 +\isamarkuptrue%
3.63 +%
3.64 +\isamarkupsubsection{terms%
3.65 +}
3.66 +\isamarkuptrue%
3.67 +%
3.68 +\isadelimML
3.69 +%
3.70 +\endisadelimML
3.71 +%
3.72 +\isatagML
3.73 +\isacommand{ML}\isamarkupfalse%
3.74 +\ {\isaliteral{7B2A}{\isacharverbatimopen}}\isanewline
3.75 +%
3.76 +\isaantiq
3.77 +term\ {\isaliteral{22}{\isachardoublequote}}{\isadigit{1}}\ {\isaliteral{3C}{\isacharless}}\ {\isaliteral{7C}{\isacharbar}}{\isaliteral{7C}{\isacharbar}}\ z\ {\isaliteral{7C}{\isacharbar}}{\isaliteral{7C}{\isacharbar}}{\isaliteral{22}{\isachardoublequote}}{}%
3.78 +\endisaantiq
3.79 +{\isaliteral{3B}{\isacharsemicolon}}\isanewline
3.80 +%
3.81 +\isaantiq
3.82 +term\ {\isaliteral{22}{\isachardoublequote}}z\ {\isaliteral{2F}{\isacharslash}}\ {\isaliteral{28}{\isacharparenleft}}z\ {\isaliteral{2D}{\isacharminus}}\ {\isadigit{1}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}{}%
3.83 +\endisaantiq
3.84 +{\isaliteral{3B}{\isacharsemicolon}}\isanewline
3.85 +%
3.86 +\isaantiq
3.87 +term\ {\isaliteral{22}{\isachardoublequote}}{\isaliteral{2D}{\isacharminus}}u\ {\isaliteral{2D}{\isacharminus}}n\ {\isaliteral{2D}{\isacharminus}}\ {\isadigit{1}}{\isaliteral{22}{\isachardoublequote}}{}%
3.88 +\endisaantiq
3.89 +{\isaliteral{3B}{\isacharsemicolon}}\isanewline
3.90 +%
3.91 +\isaantiq
3.92 +term\ {\isaliteral{22}{\isachardoublequote}}{\isaliteral{2D}{\isacharminus}}u\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{2D}{\isacharminus}}n\ {\isaliteral{2D}{\isacharminus}}\ {\isadigit{1}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{22}{\isachardoublequote}}{}%
3.93 +\endisaantiq
3.94 +{\isaliteral{3B}{\isacharsemicolon}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{5B}{\isacharbrackleft}}\ {\isaliteral{5D}{\isacharbrackright}}\ denotes\ lists\ {\isaliteral{21}{\isacharbang}}{\isaliteral{21}{\isacharbang}}{\isaliteral{21}{\isacharbang}}{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{29}{\isacharparenright}}\isanewline
3.95 +%
3.96 +\isaantiq
3.97 +term\ {\isaliteral{22}{\isachardoublequote}}z\ {\isaliteral{2F}{\isacharslash}}{\isaliteral{28}{\isacharparenleft}}z\ {\isaliteral{2D}{\isacharminus}}\ {\isadigit{1}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{2D}{\isacharminus}}u\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{2D}{\isacharminus}}n\ {\isaliteral{2D}{\isacharminus}}\ {\isadigit{1}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{22}{\isachardoublequote}}{}%
3.98 +\endisaantiq
3.99 +{\isaliteral{3B}{\isacharsemicolon}}Isac\isanewline
3.100 +%
3.101 +\isaantiq
3.102 +term\ {\isaliteral{22}{\isachardoublequote}}{\isadigit{1}}\ {\isaliteral{3C}{\isacharless}}\ {\isaliteral{7C}{\isacharbar}}{\isaliteral{7C}{\isacharbar}}\ z\ {\isaliteral{7C}{\isacharbar}}{\isaliteral{7C}{\isacharbar}}\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3E}{\isachargreater}}\ z\ {\isaliteral{2F}{\isacharslash}}\ {\isaliteral{28}{\isacharparenleft}}z\ {\isaliteral{2D}{\isacharminus}}\ {\isadigit{1}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{2D}{\isacharminus}}u\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{2D}{\isacharminus}}n\ {\isaliteral{2D}{\isacharminus}}\ {\isadigit{1}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{22}{\isachardoublequote}}{}%
3.103 +\endisaantiq
3.104 +{\isaliteral{3B}{\isacharsemicolon}}\isanewline
3.105 +term{\isadigit{2}}str\ %
3.106 +\isaantiq
3.107 +term\ {\isaliteral{22}{\isachardoublequote}}{\isadigit{1}}\ {\isaliteral{3C}{\isacharless}}\ {\isaliteral{7C}{\isacharbar}}{\isaliteral{7C}{\isacharbar}}\ z\ {\isaliteral{7C}{\isacharbar}}{\isaliteral{7C}{\isacharbar}}\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3E}{\isachargreater}}\ z\ {\isaliteral{2F}{\isacharslash}}\ {\isaliteral{28}{\isacharparenleft}}z\ {\isaliteral{2D}{\isacharminus}}\ {\isadigit{1}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{2D}{\isacharminus}}u\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{2D}{\isacharminus}}n\ {\isaliteral{2D}{\isacharminus}}\ {\isadigit{1}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{22}{\isachardoublequote}}{}%
3.108 +\endisaantiq
3.109 +{\isaliteral{3B}{\isacharsemicolon}}\isanewline
3.110 +{\isaliteral{2A7D}{\isacharverbatimclose}}\isanewline
3.111 +\isacommand{ML}\isamarkupfalse%
3.112 +\ {\isaliteral{7B2A}{\isacharverbatimopen}}\isanewline
3.113 +{\isaliteral{28}{\isacharparenleft}}{\isaliteral{2A}{\isacharasterisk}}alpha\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ \ {\isaliteral{22}{\isachardoublequote}}{\isaliteral{3C}{\isacharless}}{\isaliteral{2F}{\isacharslash}}alpha{\isaliteral{3E}{\isachargreater}}{\isaliteral{22}{\isachardoublequote}}\ {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{29}{\isacharparenright}}\isanewline
3.114 +%
3.115 +\isaantiq
3.116 +term\ {\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C616C7068613E}{\isasymalpha}}\ {\isaliteral{22}{\isachardoublequote}}{}%
3.117 +\endisaantiq
3.118 +{\isaliteral{3B}{\isacharsemicolon}}\isanewline
3.119 +%
3.120 +\isaantiq
3.121 +term\ {\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C64656C74613E}{\isasymdelta}}\ {\isaliteral{22}{\isachardoublequote}}{}%
3.122 +\endisaantiq
3.123 +{\isaliteral{3B}{\isacharsemicolon}}\isanewline
3.124 +%
3.125 +\isaantiq
3.126 +term\ {\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C7068693E}{\isasymphi}}\ {\isaliteral{22}{\isachardoublequote}}{}%
3.127 +\endisaantiq
3.128 +{\isaliteral{3B}{\isacharsemicolon}}\isanewline
3.129 +%
3.130 +\isaantiq
3.131 +term\ {\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C72686F3E}{\isasymrho}}\ {\isaliteral{22}{\isachardoublequote}}{}%
3.132 +\endisaantiq
3.133 +{\isaliteral{3B}{\isacharsemicolon}}\isanewline
3.134 +term{\isadigit{2}}str\ %
3.135 +\isaantiq
3.136 +term\ {\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C72686F3E}{\isasymrho}}\ {\isaliteral{22}{\isachardoublequote}}{}%
3.137 +\endisaantiq
3.138 +{\isaliteral{3B}{\isacharsemicolon}}\isanewline
3.139 +{\isaliteral{2A7D}{\isacharverbatimclose}}%
3.140 +\endisatagML
3.141 +{\isafoldML}%
3.142 +%
3.143 +\isadelimML
3.144 +%
3.145 +\endisadelimML
3.146 +%
3.147 +\isamarkupsubsection{rules%
3.148 +}
3.149 +\isamarkuptrue%
3.150 +\isacommand{axiomatization}\isamarkupfalse%
3.151 +\ \isakeyword{where}\ \isanewline
3.152 +\ \ rule{\isadigit{1}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isadigit{1}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{5C3C64656C74613E}{\isasymdelta}}{\isaliteral{5B}{\isacharbrackleft}}n{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{22}{\isachardoublequoteclose}}\ \isakeyword{and}\isanewline
3.153 +\ \ rule{\isadigit{2}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{7C}{\isacharbar}}{\isaliteral{7C}{\isacharbar}}\ z\ {\isaliteral{7C}{\isacharbar}}{\isaliteral{7C}{\isacharbar}}\ {\isaliteral{3E}{\isachargreater}}\ {\isadigit{1}}\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3E}{\isachargreater}}\ z\ {\isaliteral{2F}{\isacharslash}}\ {\isaliteral{28}{\isacharparenleft}}z\ {\isaliteral{2D}{\isacharminus}}\ {\isadigit{1}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ u\ {\isaliteral{5B}{\isacharbrackleft}}n{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{22}{\isachardoublequoteclose}}\ \isakeyword{and}\isanewline
3.154 +\ \ rule{\isadigit{3}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{7C}{\isacharbar}}{\isaliteral{7C}{\isacharbar}}\ z\ {\isaliteral{7C}{\isacharbar}}{\isaliteral{7C}{\isacharbar}}\ {\isaliteral{3C}{\isacharless}}\ {\isadigit{1}}\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3E}{\isachargreater}}\ z\ {\isaliteral{2F}{\isacharslash}}\ {\isaliteral{28}{\isacharparenleft}}z\ {\isaliteral{2D}{\isacharminus}}\ {\isadigit{1}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{2D}{\isacharminus}}u\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{2D}{\isacharminus}}n\ {\isaliteral{2D}{\isacharminus}}\ {\isadigit{1}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{22}{\isachardoublequoteclose}}\ \isakeyword{and}\ \isanewline
3.155 +\ \ rule{\isadigit{4}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{7C}{\isacharbar}}{\isaliteral{7C}{\isacharbar}}\ z\ {\isaliteral{7C}{\isacharbar}}{\isaliteral{7C}{\isacharbar}}\ {\isaliteral{3E}{\isachargreater}}\ {\isaliteral{7C}{\isacharbar}}{\isaliteral{7C}{\isacharbar}}\ {\isaliteral{5C3C616C7068613E}{\isasymalpha}}\ {\isaliteral{7C}{\isacharbar}}{\isaliteral{7C}{\isacharbar}}\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3E}{\isachargreater}}\ z\ {\isaliteral{2F}{\isacharslash}}\ {\isaliteral{28}{\isacharparenleft}}z\ {\isaliteral{2D}{\isacharminus}}\ {\isaliteral{5C3C616C7068613E}{\isasymalpha}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{5C3C616C7068613E}{\isasymalpha}}{\isaliteral{5E}{\isacharcircum}}{\isaliteral{5E}{\isacharcircum}}{\isaliteral{5E}{\isacharcircum}}n\ {\isaliteral{2A}{\isacharasterisk}}\ u\ {\isaliteral{5B}{\isacharbrackleft}}n{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{22}{\isachardoublequoteclose}}\ \isakeyword{and}\isanewline
3.156 +\ \ rule{\isadigit{5}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{7C}{\isacharbar}}{\isaliteral{7C}{\isacharbar}}\ z\ {\isaliteral{7C}{\isacharbar}}{\isaliteral{7C}{\isacharbar}}\ {\isaliteral{3C}{\isacharless}}\ {\isaliteral{7C}{\isacharbar}}{\isaliteral{7C}{\isacharbar}}\ {\isaliteral{5C3C616C7068613E}{\isasymalpha}}\ {\isaliteral{7C}{\isacharbar}}{\isaliteral{7C}{\isacharbar}}\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3E}{\isachargreater}}\ z\ {\isaliteral{2F}{\isacharslash}}\ {\isaliteral{28}{\isacharparenleft}}z\ {\isaliteral{2D}{\isacharminus}}\ {\isaliteral{5C3C616C7068613E}{\isasymalpha}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C616C7068613E}{\isasymalpha}}{\isaliteral{5E}{\isacharcircum}}{\isaliteral{5E}{\isacharcircum}}{\isaliteral{5E}{\isacharcircum}}n{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{2A}{\isacharasterisk}}\ u\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{2D}{\isacharminus}}n\ {\isaliteral{2D}{\isacharminus}}\ {\isadigit{1}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{22}{\isachardoublequoteclose}}\ \isakeyword{and}\isanewline
3.157 +\ \ rule{\isadigit{6}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{7C}{\isacharbar}}{\isaliteral{7C}{\isacharbar}}\ z\ {\isaliteral{7C}{\isacharbar}}{\isaliteral{7C}{\isacharbar}}\ {\isaliteral{3E}{\isachargreater}}\ {\isadigit{1}}\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3E}{\isachargreater}}\ z{\isaliteral{2F}{\isacharslash}}{\isaliteral{28}{\isacharparenleft}}z\ {\isaliteral{2D}{\isacharminus}}\ {\isadigit{1}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{5E}{\isacharcircum}}{\isaliteral{5E}{\isacharcircum}}{\isaliteral{5E}{\isacharcircum}}{\isadigit{2}}\ {\isaliteral{3D}{\isacharequal}}\ n\ {\isaliteral{2A}{\isacharasterisk}}\ u\ {\isaliteral{5B}{\isacharbrackleft}}n{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
3.158 +%
3.159 +\isadelimML
3.160 +%
3.161 +\endisadelimML
3.162 +%
3.163 +\isatagML
3.164 +\isacommand{ML}\isamarkupfalse%
3.165 +\ {\isaliteral{7B2A}{\isacharverbatimopen}}\isanewline
3.166 +%
3.167 +\isaantiq
3.168 +thm\ rule{\isadigit{1}}{}%
3.169 +\endisaantiq
3.170 +{\isaliteral{3B}{\isacharsemicolon}}\isanewline
3.171 +%
3.172 +\isaantiq
3.173 +thm\ rule{\isadigit{2}}{}%
3.174 +\endisaantiq
3.175 +{\isaliteral{3B}{\isacharsemicolon}}\isanewline
3.176 +%
3.177 +\isaantiq
3.178 +thm\ rule{\isadigit{3}}{}%
3.179 +\endisaantiq
3.180 +{\isaliteral{3B}{\isacharsemicolon}}\isanewline
3.181 +%
3.182 +\isaantiq
3.183 +thm\ rule{\isadigit{4}}{}%
3.184 +\endisaantiq
3.185 +{\isaliteral{3B}{\isacharsemicolon}}\isanewline
3.186 +{\isaliteral{2A7D}{\isacharverbatimclose}}%
3.187 +\endisatagML
3.188 +{\isafoldML}%
3.189 +%
3.190 +\isadelimML
3.191 +%
3.192 +\endisadelimML
3.193 +%
3.194 +\isamarkupsubsection{apply rules%
3.195 +}
3.196 +\isamarkuptrue%
3.197 +%
3.198 +\isadelimML
3.199 +%
3.200 +\endisadelimML
3.201 +%
3.202 +\isatagML
3.203 +\isacommand{ML}\isamarkupfalse%
3.204 +\ {\isaliteral{7B2A}{\isacharverbatimopen}}\isanewline
3.205 +val\ inverse{\isaliteral{5F}{\isacharunderscore}}Z\ {\isaliteral{3D}{\isacharequal}}\ append{\isaliteral{5F}{\isacharunderscore}}rls\ {\isaliteral{22}{\isachardoublequote}}inverse{\isaliteral{5F}{\isacharunderscore}}Z{\isaliteral{22}{\isachardoublequote}}\ e{\isaliteral{5F}{\isacharunderscore}}rls\isanewline
3.206 +\ \ {\isaliteral{5B}{\isacharbrackleft}}\ Thm\ \ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{22}{\isachardoublequote}}rule{\isadigit{3}}{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}num{\isaliteral{5F}{\isacharunderscore}}str\ %
3.207 +\isaantiq
3.208 +thm\ rule{\isadigit{3}}{}%
3.209 +\endisaantiq
3.210 +{\isaliteral{29}{\isacharparenright}}{\isaliteral{2C}{\isacharcomma}}\isanewline
3.211 +\ \ \ \ Thm\ \ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{22}{\isachardoublequote}}rule{\isadigit{4}}{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}num{\isaliteral{5F}{\isacharunderscore}}str\ %
3.212 +\isaantiq
3.213 +thm\ rule{\isadigit{4}}{}%
3.214 +\endisaantiq
3.215 +{\isaliteral{29}{\isacharparenright}}{\isaliteral{2C}{\isacharcomma}}\isanewline
3.216 +\ \ \ \ Thm\ \ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{22}{\isachardoublequote}}rule{\isadigit{1}}{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}num{\isaliteral{5F}{\isacharunderscore}}str\ %
3.217 +\isaantiq
3.218 +thm\ rule{\isadigit{1}}{}%
3.219 +\endisaantiq
3.220 +{\isaliteral{29}{\isacharparenright}}\ \ \ \isanewline
3.221 +\ \ {\isaliteral{5D}{\isacharbrackright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
3.222 +\isanewline
3.223 +val\ t\ {\isaliteral{3D}{\isacharequal}}\ str{\isadigit{2}}term\ {\isaliteral{22}{\isachardoublequote}}z\ {\isaliteral{2F}{\isacharslash}}\ {\isaliteral{28}{\isacharparenleft}}z\ {\isaliteral{2D}{\isacharminus}}\ {\isadigit{1}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{2B}{\isacharplus}}\ z\ {\isaliteral{2F}{\isacharslash}}\ {\isaliteral{28}{\isacharparenleft}}z\ {\isaliteral{2D}{\isacharminus}}\ {\isaliteral{5C3C616C7068613E}{\isasymalpha}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{2B}{\isacharplus}}\ {\isadigit{1}}{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
3.224 +val\ SOME\ {\isaliteral{28}{\isacharparenleft}}t{\isaliteral{27}{\isacharprime}}{\isaliteral{2C}{\isacharcomma}}\ asm{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ rewrite{\isaliteral{5F}{\isacharunderscore}}set{\isaliteral{5F}{\isacharunderscore}}\ thy\ true\ inverse{\isaliteral{5F}{\isacharunderscore}}Z\ t{\isaliteral{3B}{\isacharsemicolon}}\isanewline
3.225 +term{\isadigit{2}}str\ t{\isaliteral{27}{\isacharprime}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{22}{\isachardoublequote}}z\ {\isaliteral{2F}{\isacharslash}}\ {\isaliteral{28}{\isacharparenleft}}z\ {\isaliteral{2D}{\isacharminus}}\ {\isaliteral{3F}{\isacharquery}}{\isaliteral{5C3C64656C74613E}{\isasymdelta}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{3F}{\isacharquery}}n{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{2B}{\isacharplus}}\ z\ {\isaliteral{2F}{\isacharslash}}\ {\isaliteral{28}{\isacharparenleft}}z\ {\isaliteral{2D}{\isacharminus}}\ {\isaliteral{5C3C616C7068613E}{\isasymalpha}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{2B}{\isacharplus}}\ {\isaliteral{3F}{\isacharquery}}{\isaliteral{5C3C64656C74613E}{\isasymdelta}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{3F}{\isacharquery}}n{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3B}{\isacharsemicolon}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{2A}{\isacharasterisk}}attention\ rule{\isadigit{1}}\ {\isaliteral{21}{\isacharbang}}{\isaliteral{21}{\isacharbang}}{\isaliteral{21}{\isacharbang}}{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{29}{\isacharparenright}}\isanewline
3.226 +{\isaliteral{2A7D}{\isacharverbatimclose}}\isanewline
3.227 +\isacommand{ML}\isamarkupfalse%
3.228 +\ {\isaliteral{7B2A}{\isacharverbatimopen}}\isanewline
3.229 +val\ {\isaliteral{28}{\isacharparenleft}}thy{\isaliteral{2C}{\isacharcomma}}\ ro{\isaliteral{2C}{\isacharcomma}}\ er{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}%
3.230 +\isaantiq
3.231 +theory\ Isac{}%
3.232 +\endisaantiq
3.233 +{\isaliteral{2C}{\isacharcomma}}\ tless{\isaliteral{5F}{\isacharunderscore}}true{\isaliteral{2C}{\isacharcomma}}\ eval{\isaliteral{5F}{\isacharunderscore}}rls{\isaliteral{29}{\isacharparenright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
3.234 +{\isaliteral{2A7D}{\isacharverbatimclose}}\isanewline
3.235 +\isacommand{ML}\isamarkupfalse%
3.236 +\ {\isaliteral{7B2A}{\isacharverbatimopen}}\isanewline
3.237 +val\ SOME\ {\isaliteral{28}{\isacharparenleft}}t{\isaliteral{2C}{\isacharcomma}}\ asm{\isadigit{1}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ rewrite{\isaliteral{5F}{\isacharunderscore}}\ thy\ ro\ er\ true\ {\isaliteral{28}{\isacharparenleft}}num{\isaliteral{5F}{\isacharunderscore}}str\ %
3.238 +\isaantiq
3.239 +thm\ rule{\isadigit{3}}{}%
3.240 +\endisaantiq
3.241 +{\isaliteral{29}{\isacharparenright}}\ t{\isaliteral{3B}{\isacharsemicolon}}\isanewline
3.242 +term{\isadigit{2}}str\ t\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{22}{\isachardoublequote}}{\isaliteral{2D}{\isacharminus}}\ {\isaliteral{3F}{\isacharquery}}u\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{2D}{\isacharminus}}\ {\isaliteral{3F}{\isacharquery}}n\ {\isaliteral{2D}{\isacharminus}}\ {\isadigit{1}}{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{2B}{\isacharplus}}\ z\ {\isaliteral{2F}{\isacharslash}}\ {\isaliteral{28}{\isacharparenleft}}z\ {\isaliteral{2D}{\isacharminus}}\ {\isaliteral{5C3C616C7068613E}{\isasymalpha}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{2B}{\isacharplus}}\ {\isadigit{1}}{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3B}{\isacharsemicolon}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{2D}{\isacharminus}}\ real\ {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{29}{\isacharparenright}}\isanewline
3.243 +term{\isadigit{2}}str\ t{\isaliteral{3B}{\isacharsemicolon}}\isanewline
3.244 +{\isaliteral{2A7D}{\isacharverbatimclose}}\isanewline
3.245 +\isacommand{ML}\isamarkupfalse%
3.246 +\ {\isaliteral{7B2A}{\isacharverbatimopen}}\isanewline
3.247 +val\ SOME\ {\isaliteral{28}{\isacharparenleft}}t{\isaliteral{2C}{\isacharcomma}}\ asm{\isadigit{2}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ rewrite{\isaliteral{5F}{\isacharunderscore}}\ thy\ ro\ er\ true\ {\isaliteral{28}{\isacharparenleft}}num{\isaliteral{5F}{\isacharunderscore}}str\ %
3.248 +\isaantiq
3.249 +thm\ rule{\isadigit{4}}{}%
3.250 +\endisaantiq
3.251 +{\isaliteral{29}{\isacharparenright}}\ t{\isaliteral{3B}{\isacharsemicolon}}\isanewline
3.252 +term{\isadigit{2}}str\ t\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{22}{\isachardoublequote}}{\isaliteral{2D}{\isacharminus}}\ {\isaliteral{3F}{\isacharquery}}u\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{2D}{\isacharminus}}\ {\isaliteral{3F}{\isacharquery}}n\ {\isaliteral{2D}{\isacharminus}}\ {\isadigit{1}}{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{2B}{\isacharplus}}\ {\isaliteral{5C3C616C7068613E}{\isasymalpha}}\ {\isaliteral{5E}{\isacharcircum}}{\isaliteral{5E}{\isacharcircum}}{\isaliteral{5E}{\isacharcircum}}\ {\isaliteral{3F}{\isacharquery}}n\ {\isaliteral{2A}{\isacharasterisk}}\ {\isaliteral{3F}{\isacharquery}}u\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{3F}{\isacharquery}}n{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{2B}{\isacharplus}}\ {\isadigit{1}}{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3B}{\isacharsemicolon}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{2D}{\isacharminus}}\ real\ {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{29}{\isacharparenright}}\isanewline
3.253 +term{\isadigit{2}}str\ t{\isaliteral{3B}{\isacharsemicolon}}\isanewline
3.254 +{\isaliteral{2A7D}{\isacharverbatimclose}}\isanewline
3.255 +\isacommand{ML}\isamarkupfalse%
3.256 +\ {\isaliteral{7B2A}{\isacharverbatimopen}}\isanewline
3.257 +val\ SOME\ {\isaliteral{28}{\isacharparenleft}}t{\isaliteral{2C}{\isacharcomma}}\ asm{\isadigit{3}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ rewrite{\isaliteral{5F}{\isacharunderscore}}\ thy\ ro\ er\ true\ {\isaliteral{28}{\isacharparenleft}}num{\isaliteral{5F}{\isacharunderscore}}str\ %
3.258 +\isaantiq
3.259 +thm\ rule{\isadigit{1}}{}%
3.260 +\endisaantiq
3.261 +{\isaliteral{29}{\isacharparenright}}\ t{\isaliteral{3B}{\isacharsemicolon}}\isanewline
3.262 +term{\isadigit{2}}str\ t\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{22}{\isachardoublequote}}{\isaliteral{2D}{\isacharminus}}\ {\isaliteral{3F}{\isacharquery}}u\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{2D}{\isacharminus}}\ {\isaliteral{3F}{\isacharquery}}n\ {\isaliteral{2D}{\isacharminus}}\ {\isadigit{1}}{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{2B}{\isacharplus}}\ {\isaliteral{5C3C616C7068613E}{\isasymalpha}}\ {\isaliteral{5E}{\isacharcircum}}{\isaliteral{5E}{\isacharcircum}}{\isaliteral{5E}{\isacharcircum}}\ {\isaliteral{3F}{\isacharquery}}n\ {\isaliteral{2A}{\isacharasterisk}}\ {\isaliteral{3F}{\isacharquery}}u\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{3F}{\isacharquery}}n{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{2B}{\isacharplus}}\ {\isaliteral{3F}{\isacharquery}}{\isaliteral{5C3C64656C74613E}{\isasymdelta}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{3F}{\isacharquery}}n{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3B}{\isacharsemicolon}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{2D}{\isacharminus}}\ real\ {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{29}{\isacharparenright}}\isanewline
3.263 +term{\isadigit{2}}str\ t{\isaliteral{3B}{\isacharsemicolon}}\isanewline
3.264 +{\isaliteral{2A7D}{\isacharverbatimclose}}\isanewline
3.265 +\isacommand{ML}\isamarkupfalse%
3.266 +\ {\isaliteral{7B2A}{\isacharverbatimopen}}\isanewline
3.267 +terms{\isadigit{2}}str\ {\isaliteral{28}{\isacharparenleft}}asm{\isadigit{1}}\ {\isaliteral{40}{\isacharat}}\ asm{\isadigit{2}}\ {\isaliteral{40}{\isacharat}}\ asm{\isadigit{3}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
3.268 +{\isaliteral{2A7D}{\isacharverbatimclose}}%
3.269 +\endisatagML
3.270 +{\isafoldML}%
3.271 +%
3.272 +\isadelimML
3.273 +%
3.274 +\endisadelimML
3.275 +%
3.276 +\isamarkupsection{Prepare steps in CTP-based programming language%
3.277 +}
3.278 +\isamarkuptrue%
3.279 +%
3.280 +\begin{isamarkuptext}%
3.281 +===================================================%
3.282 +\end{isamarkuptext}%
3.283 +\isamarkuptrue%
3.284 +%
3.285 +\isamarkupsubsection{prepare expression%
3.286 +}
3.287 +\isamarkuptrue%
3.288 +%
3.289 +\isadelimML
3.290 +%
3.291 +\endisadelimML
3.292 +%
3.293 +\isatagML
3.294 +\isacommand{ML}\isamarkupfalse%
3.295 +\ {\isaliteral{7B2A}{\isacharverbatimopen}}\isanewline
3.296 +val\ ctxt\ {\isaliteral{3D}{\isacharequal}}\ ProofContext{\isaliteral{2E}{\isachardot}}init{\isaliteral{5F}{\isacharunderscore}}global\ %
3.297 +\isaantiq
3.298 +theory\ Isac{}%
3.299 +\endisaantiq
3.300 +{\isaliteral{3B}{\isacharsemicolon}}\isanewline
3.301 +val\ ctxt\ {\isaliteral{3D}{\isacharequal}}\ declare{\isaliteral{5F}{\isacharunderscore}}constraints{\isaliteral{27}{\isacharprime}}\ {\isaliteral{5B}{\isacharbrackleft}}%
3.302 +\isaantiq
3.303 +term\ {\isaliteral{22}{\isachardoublequote}}z{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}real{\isaliteral{22}{\isachardoublequote}}{}%
3.304 +\endisaantiq
3.305 +{\isaliteral{5D}{\isacharbrackright}}\ ctxt{\isaliteral{3B}{\isacharsemicolon}}\isanewline
3.306 +\isanewline
3.307 +val\ SOME\ fun{\isadigit{1}}\ {\isaliteral{3D}{\isacharequal}}\ parseNEW\ ctxt\ {\isaliteral{22}{\isachardoublequote}}X\ z\ {\isaliteral{3D}{\isacharequal}}\ {\isadigit{3}}\ {\isaliteral{2F}{\isacharslash}}\ {\isaliteral{28}{\isacharparenleft}}z\ {\isaliteral{2D}{\isacharminus}}\ {\isadigit{1}}{\isaliteral{2F}{\isacharslash}}{\isadigit{4}}\ {\isaliteral{2B}{\isacharplus}}\ {\isaliteral{2D}{\isacharminus}}{\isadigit{1}}{\isaliteral{2F}{\isacharslash}}{\isadigit{8}}\ {\isaliteral{2A}{\isacharasterisk}}\ z\ {\isaliteral{5E}{\isacharcircum}}{\isaliteral{5E}{\isacharcircum}}{\isaliteral{5E}{\isacharcircum}}\ {\isaliteral{2D}{\isacharminus}}{\isadigit{1}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3B}{\isacharsemicolon}}\ term{\isadigit{2}}str\ fun{\isadigit{1}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
3.308 +val\ SOME\ fun{\isadigit{1}}{\isaliteral{27}{\isacharprime}}\ {\isaliteral{3D}{\isacharequal}}\ parseNEW\ ctxt\ {\isaliteral{22}{\isachardoublequote}}X\ z\ {\isaliteral{3D}{\isacharequal}}\ {\isadigit{3}}\ {\isaliteral{2F}{\isacharslash}}\ {\isaliteral{28}{\isacharparenleft}}z\ {\isaliteral{2D}{\isacharminus}}\ {\isadigit{1}}{\isaliteral{2F}{\isacharslash}}{\isadigit{4}}\ {\isaliteral{2B}{\isacharplus}}\ {\isaliteral{2D}{\isacharminus}}{\isadigit{1}}{\isaliteral{2F}{\isacharslash}}{\isadigit{8}}\ {\isaliteral{2A}{\isacharasterisk}}\ {\isaliteral{28}{\isacharparenleft}}{\isadigit{1}}{\isaliteral{2F}{\isacharslash}}z{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3B}{\isacharsemicolon}}\ term{\isadigit{2}}str\ fun{\isadigit{1}}{\isaliteral{27}{\isacharprime}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
3.309 +{\isaliteral{2A7D}{\isacharverbatimclose}}%
3.310 +\endisatagML
3.311 +{\isafoldML}%
3.312 +%
3.313 +\isadelimML
3.314 +%
3.315 +\endisadelimML
3.316 +\isanewline
3.317 +\isanewline
3.318 +\isacommand{axiomatization}\isamarkupfalse%
3.319 +\ \isakeyword{where}\isanewline
3.320 +\ \ ruleZY{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{28}{\isacharparenleft}}X\ z\ {\isaliteral{3D}{\isacharequal}}\ a\ {\isaliteral{2F}{\isacharslash}}\ b{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}X{\isaliteral{27}{\isacharprime}}\ z\ {\isaliteral{3D}{\isacharequal}}\ a\ {\isaliteral{2F}{\isacharslash}}\ {\isaliteral{28}{\isacharparenleft}}z\ {\isaliteral{2A}{\isacharasterisk}}\ b{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
3.321 +%
3.322 +\isadelimML
3.323 +\isanewline
3.324 +%
3.325 +\endisadelimML
3.326 +%
3.327 +\isatagML
3.328 +\isacommand{ML}\isamarkupfalse%
3.329 +\ {\isaliteral{7B2A}{\isacharverbatimopen}}\isanewline
3.330 +val\ {\isaliteral{28}{\isacharparenleft}}thy{\isaliteral{2C}{\isacharcomma}}\ ro{\isaliteral{2C}{\isacharcomma}}\ er{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}%
3.331 +\isaantiq
3.332 +theory\ Isac{}%
3.333 +\endisaantiq
3.334 +{\isaliteral{2C}{\isacharcomma}}\ tless{\isaliteral{5F}{\isacharunderscore}}true{\isaliteral{2C}{\isacharcomma}}\ eval{\isaliteral{5F}{\isacharunderscore}}rls{\isaliteral{29}{\isacharparenright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
3.335 +val\ SOME\ {\isaliteral{28}{\isacharparenleft}}fun{\isadigit{2}}{\isaliteral{2C}{\isacharcomma}}\ asm{\isadigit{1}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ rewrite{\isaliteral{5F}{\isacharunderscore}}\ thy\ ro\ er\ true\ \ %
3.336 +\isaantiq
3.337 +thm\ ruleZY{}%
3.338 +\endisaantiq
3.339 +\ fun{\isadigit{1}}{\isaliteral{3B}{\isacharsemicolon}}\ term{\isadigit{2}}str\ fun{\isadigit{2}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
3.340 +val\ SOME\ {\isaliteral{28}{\isacharparenleft}}fun{\isadigit{2}}{\isaliteral{27}{\isacharprime}}{\isaliteral{2C}{\isacharcomma}}\ asm{\isadigit{1}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ rewrite{\isaliteral{5F}{\isacharunderscore}}\ thy\ ro\ er\ true\ \ %
3.341 +\isaantiq
3.342 +thm\ ruleZY{}%
3.343 +\endisaantiq
3.344 +\ fun{\isadigit{1}}{\isaliteral{27}{\isacharprime}}{\isaliteral{3B}{\isacharsemicolon}}\ term{\isadigit{2}}str\ fun{\isadigit{2}}{\isaliteral{27}{\isacharprime}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
3.345 +\isanewline
3.346 +val\ SOME\ {\isaliteral{28}{\isacharparenleft}}fun{\isadigit{3}}{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ rewrite{\isaliteral{5F}{\isacharunderscore}}set{\isaliteral{5F}{\isacharunderscore}}\ %
3.347 +\isaantiq
3.348 +theory\ Isac{}%
3.349 +\endisaantiq
3.350 +\ false\ norm{\isaliteral{5F}{\isacharunderscore}}Rational\ fun{\isadigit{2}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
3.351 +term{\isadigit{2}}str\ fun{\isadigit{3}}{\isaliteral{3B}{\isacharsemicolon}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{2A}{\isacharasterisk}}fails\ on\ x{\isaliteral{5E}{\isacharcircum}}{\isaliteral{5E}{\isacharcircum}}{\isaliteral{5E}{\isacharcircum}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{2D}{\isacharminus}}{\isadigit{1}}{\isaliteral{29}{\isacharparenright}}\ TODO{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{29}{\isacharparenright}}\isanewline
3.352 +val\ SOME\ {\isaliteral{28}{\isacharparenleft}}fun{\isadigit{3}}{\isaliteral{27}{\isacharprime}}{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ rewrite{\isaliteral{5F}{\isacharunderscore}}set{\isaliteral{5F}{\isacharunderscore}}\ %
3.353 +\isaantiq
3.354 +theory\ Isac{}%
3.355 +\endisaantiq
3.356 +\ false\ norm{\isaliteral{5F}{\isacharunderscore}}Rational\ fun{\isadigit{2}}{\isaliteral{27}{\isacharprime}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
3.357 +term{\isadigit{2}}str\ fun{\isadigit{3}}{\isaliteral{27}{\isacharprime}}{\isaliteral{3B}{\isacharsemicolon}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{2A}{\isacharasterisk}}OK{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{29}{\isacharparenright}}\isanewline
3.358 +\isanewline
3.359 +val\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}\ expr{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ HOLogic{\isaliteral{2E}{\isachardot}}dest{\isaliteral{5F}{\isacharunderscore}}eq\ fun{\isadigit{3}}{\isaliteral{27}{\isacharprime}}{\isaliteral{3B}{\isacharsemicolon}}\ term{\isadigit{2}}str\ expr{\isaliteral{3B}{\isacharsemicolon}}\isanewline
3.360 +{\isaliteral{2A7D}{\isacharverbatimclose}}%
3.361 +\endisatagML
3.362 +{\isafoldML}%
3.363 +%
3.364 +\isadelimML
3.365 +%
3.366 +\endisadelimML
3.367 +%
3.368 +\isamarkupsubsection{solve equation%
3.369 +}
3.370 +\isamarkuptrue%
3.371 +%
3.372 +\begin{isamarkuptext}%
3.373 +this type of equation if too general for the present program%
3.374 +\end{isamarkuptext}%
3.375 +\isamarkuptrue%
3.376 +%
3.377 +\isadelimML
3.378 +%
3.379 +\endisadelimML
3.380 +%
3.381 +\isatagML
3.382 +\isacommand{ML}\isamarkupfalse%
3.383 +\ {\isaliteral{7B2A}{\isacharverbatimopen}}\isanewline
3.384 +{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2D}{\isacharminus}}{\isaliteral{2D}{\isacharminus}}{\isaliteral{2D}{\isacharminus}}{\isaliteral{2D}{\isacharminus}}{\isaliteral{2D}{\isacharminus}}{\isaliteral{2D}{\isacharminus}}{\isaliteral{2D}{\isacharminus}}{\isaliteral{2D}{\isacharminus}}{\isaliteral{2D}{\isacharminus}}{\isaliteral{2D}{\isacharminus}}{\isaliteral{2D}{\isacharminus}}\ Minisubplb{\isaliteral{2F}{\isacharslash}}{\isadigit{1}}{\isadigit{0}}{\isadigit{0}}{\isaliteral{2D}{\isacharminus}}init{\isaliteral{2D}{\isacharminus}}rootp\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{2A}{\isacharasterisk}}OK{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{29}{\isacharparenright}}bl{\isaliteral{2E}{\isachardot}}sml\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{2D}{\isacharminus}}{\isaliteral{2D}{\isacharminus}}{\isaliteral{2D}{\isacharminus}}{\isaliteral{2D}{\isacharminus}}{\isaliteral{2D}{\isacharminus}}{\isaliteral{2D}{\isacharminus}}{\isaliteral{2D}{\isacharminus}}{\isaliteral{2D}{\isacharminus}}{\isaliteral{2D}{\isacharminus}}{\isaliteral{2D}{\isacharminus}}{\isaliteral{2D}{\isacharminus}}{\isaliteral{2D}{\isacharminus}}{\isaliteral{2D}{\isacharminus}}{\isaliteral{2D}{\isacharminus}}{\isaliteral{2D}{\isacharminus}}{\isaliteral{2D}{\isacharminus}}{\isaliteral{2D}{\isacharminus}}{\isaliteral{2D}{\isacharminus}}{\isaliteral{2D}{\isacharminus}}{\isaliteral{2D}{\isacharminus}}{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
3.385 +val\ denominator\ {\isaliteral{3D}{\isacharequal}}\ parseNEW\ ctxt\ {\isaliteral{22}{\isachardoublequote}}z{\isaliteral{5E}{\isacharcircum}}{\isaliteral{5E}{\isacharcircum}}{\isaliteral{5E}{\isacharcircum}}{\isadigit{2}}\ {\isaliteral{2D}{\isacharminus}}\ {\isadigit{1}}{\isaliteral{2F}{\isacharslash}}{\isadigit{4}}{\isaliteral{2A}{\isacharasterisk}}z\ {\isaliteral{2D}{\isacharminus}}\ {\isadigit{1}}{\isaliteral{2F}{\isacharslash}}{\isadigit{8}}\ {\isaliteral{3D}{\isacharequal}}\ {\isadigit{0}}{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
3.386 +val\ fmz\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{22}{\isachardoublequote}}equality\ {\isaliteral{28}{\isacharparenleft}}z{\isaliteral{5E}{\isacharcircum}}{\isaliteral{5E}{\isacharcircum}}{\isaliteral{5E}{\isacharcircum}}{\isadigit{2}}\ {\isaliteral{2D}{\isacharminus}}\ {\isadigit{1}}{\isaliteral{2F}{\isacharslash}}{\isadigit{4}}{\isaliteral{2A}{\isacharasterisk}}z\ {\isaliteral{2D}{\isacharminus}}\ {\isadigit{1}}{\isaliteral{2F}{\isacharslash}}{\isadigit{8}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}{\isadigit{0}}{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}real{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{22}{\isachardoublequote}}solveFor\ z{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}{\isaliteral{22}{\isachardoublequote}}solutions\ L{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
3.387 +val\ {\isaliteral{28}{\isacharparenleft}}dI{\isaliteral{27}{\isacharprime}}{\isaliteral{2C}{\isacharcomma}}pI{\isaliteral{27}{\isacharprime}}{\isaliteral{2C}{\isacharcomma}}mI{\isaliteral{27}{\isacharprime}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{22}{\isachardoublequote}}Isac{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{22}{\isachardoublequote}}univariate{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}{\isaliteral{22}{\isachardoublequote}}equation{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{22}{\isachardoublequote}}no{\isaliteral{5F}{\isacharunderscore}}met{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
3.388 +{\isaliteral{28}{\isacharparenleft}}{\isaliteral{2A}{\isacharasterisk}}\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isaliteral{5E}{\isacharcircum}}{\isaliteral{5E}{\isacharcircum}}{\isaliteral{5E}{\isacharcircum}}{\isaliteral{5E}{\isacharcircum}}{\isaliteral{5E}{\isacharcircum}}{\isaliteral{5E}{\isacharcircum}}{\isaliteral{5E}{\isacharcircum}}{\isaliteral{5E}{\isacharcircum}}{\isaliteral{5E}{\isacharcircum}}{\isaliteral{5E}{\isacharcircum}}{\isaliteral{5E}{\isacharcircum}}{\isaliteral{5E}{\isacharcircum}}{\isaliteral{5E}{\isacharcircum}}{\isaliteral{5E}{\isacharcircum}}{\isaliteral{5E}{\isacharcircum}}{\isaliteral{5E}{\isacharcircum}}{\isaliteral{5E}{\isacharcircum}}{\isaliteral{5E}{\isacharcircum}}{\isaliteral{5E}{\isacharcircum}}{\isaliteral{5E}{\isacharcircum}}{\isaliteral{5E}{\isacharcircum}}{\isaliteral{5E}{\isacharcircum}}\ TODO{\isaliteral{3A}{\isacharcolon}}\ ISAC\ determines\ type\ of\ eq{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{29}{\isacharparenright}}\isanewline
3.389 +{\isaliteral{2A7D}{\isacharverbatimclose}}%
3.390 +\endisatagML
3.391 +{\isafoldML}%
3.392 +%
3.393 +\isadelimML
3.394 +%
3.395 +\endisadelimML
3.396 +%
3.397 +\begin{isamarkuptext}%
3.398 +Does the Equation Match the Specification ?%
3.399 +\end{isamarkuptext}%
3.400 +\isamarkuptrue%
3.401 +%
3.402 +\isadelimML
3.403 +%
3.404 +\endisadelimML
3.405 +%
3.406 +\isatagML
3.407 +\isacommand{ML}\isamarkupfalse%
3.408 +\ {\isaliteral{7B2A}{\isacharverbatimopen}}\isanewline
3.409 +match{\isaliteral{5F}{\isacharunderscore}}pbl\ fmz\ {\isaliteral{28}{\isacharparenleft}}get{\isaliteral{5F}{\isacharunderscore}}pbt\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{22}{\isachardoublequote}}univariate{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}{\isaliteral{22}{\isachardoublequote}}equation{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
3.410 +{\isaliteral{2A7D}{\isacharverbatimclose}}\isanewline
3.411 +\isacommand{ML}\isamarkupfalse%
3.412 +\ {\isaliteral{7B2A}{\isacharverbatimopen}}Context{\isaliteral{2E}{\isachardot}}theory{\isaliteral{5F}{\isacharunderscore}}name\ thy\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{22}{\isachardoublequote}}Isac{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{2A7D}{\isacharverbatimclose}}\isanewline
3.413 +\isanewline
3.414 +\isacommand{ML}\isamarkupfalse%
3.415 +\ {\isaliteral{7B2A}{\isacharverbatimopen}}\isanewline
3.416 +val\ denominator\ {\isaliteral{3D}{\isacharequal}}\ parseNEW\ ctxt\ {\isaliteral{22}{\isachardoublequote}}{\isaliteral{2D}{\isacharminus}}{\isadigit{1}}{\isaliteral{2F}{\isacharslash}}{\isadigit{8}}\ {\isaliteral{2B}{\isacharplus}}\ {\isaliteral{2D}{\isacharminus}}{\isadigit{1}}{\isaliteral{2F}{\isacharslash}}{\isadigit{4}}{\isaliteral{2A}{\isacharasterisk}}z\ {\isaliteral{2B}{\isacharplus}}\ z{\isaliteral{5E}{\isacharcircum}}{\isaliteral{5E}{\isacharcircum}}{\isaliteral{5E}{\isacharcircum}}{\isadigit{2}}\ {\isaliteral{3D}{\isacharequal}}\ {\isadigit{0}}{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
3.417 +val\ fmz\ {\isaliteral{3D}{\isacharequal}}\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{2A}{\isacharasterisk}}specification{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{29}{\isacharparenright}}\isanewline
3.418 +\ \ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{22}{\isachardoublequote}}equality\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{2D}{\isacharminus}}{\isadigit{1}}{\isaliteral{2F}{\isacharslash}}{\isadigit{8}}\ {\isaliteral{2B}{\isacharplus}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{2D}{\isacharminus}}{\isadigit{1}}{\isaliteral{2F}{\isacharslash}}{\isadigit{4}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{2A}{\isacharasterisk}}z\ {\isaliteral{2B}{\isacharplus}}\ z{\isaliteral{5E}{\isacharcircum}}{\isaliteral{5E}{\isacharcircum}}{\isaliteral{5E}{\isacharcircum}}{\isadigit{2}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}{\isadigit{0}}{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}real{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{2A}{\isacharasterisk}}equality{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{29}{\isacharparenright}}\isanewline
3.419 +\ \ \ {\isaliteral{22}{\isachardoublequote}}solveFor\ z{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{2A}{\isacharasterisk}}bound\ variable{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{29}{\isacharparenright}}\isanewline
3.420 +\ \ \ {\isaliteral{22}{\isachardoublequote}}solutions\ L{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{3B}{\isacharsemicolon}}\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{2A}{\isacharasterisk}}identifier\ for\ solution{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{29}{\isacharparenright}}\isanewline
3.421 +{\isaliteral{28}{\isacharparenleft}}{\isaliteral{2A}{\isacharasterisk}}liste\ der\ theoreme\ die\ zum\ lösen\ benötigt\ werden{\isaliteral{2C}{\isacharcomma}}\ aus\ isac{\isaliteral{2C}{\isacharcomma}}\ keine\ spezielle\ methode\ {\isaliteral{28}{\isacharparenleft}}no\ met{\isaliteral{29}{\isacharparenright}}{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{29}{\isacharparenright}}\isanewline
3.422 +val\ {\isaliteral{28}{\isacharparenleft}}dI{\isaliteral{27}{\isacharprime}}{\isaliteral{2C}{\isacharcomma}}pI{\isaliteral{27}{\isacharprime}}{\isaliteral{2C}{\isacharcomma}}mI{\isaliteral{27}{\isacharprime}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\isanewline
3.423 +\ \ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{22}{\isachardoublequote}}Isac{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{22}{\isachardoublequote}}pqFormula{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}{\isaliteral{22}{\isachardoublequote}}degree{\isaliteral{5F}{\isacharunderscore}}{\isadigit{2}}{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}{\isaliteral{22}{\isachardoublequote}}polynomial{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}{\isaliteral{22}{\isachardoublequote}}univariate{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}{\isaliteral{22}{\isachardoublequote}}equation{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{22}{\isachardoublequote}}no{\isaliteral{5F}{\isacharunderscore}}met{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
3.424 +{\isaliteral{2A7D}{\isacharverbatimclose}}%
3.425 +\endisatagML
3.426 +{\isafoldML}%
3.427 +%
3.428 +\isadelimML
3.429 +%
3.430 +\endisadelimML
3.431 +%
3.432 +\begin{isamarkuptext}%
3.433 +Does the Other Equation Match the Specification ?%
3.434 +\end{isamarkuptext}%
3.435 +\isamarkuptrue%
3.436 +%
3.437 +\isadelimML
3.438 +%
3.439 +\endisadelimML
3.440 +%
3.441 +\isatagML
3.442 +\isacommand{ML}\isamarkupfalse%
3.443 +\ {\isaliteral{7B2A}{\isacharverbatimopen}}\isanewline
3.444 +match{\isaliteral{5F}{\isacharunderscore}}pbl\ fmz\ {\isaliteral{28}{\isacharparenleft}}get{\isaliteral{5F}{\isacharunderscore}}pbt\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{22}{\isachardoublequote}}pqFormula{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}{\isaliteral{22}{\isachardoublequote}}degree{\isaliteral{5F}{\isacharunderscore}}{\isadigit{2}}{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}{\isaliteral{22}{\isachardoublequote}}polynomial{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}{\isaliteral{22}{\isachardoublequote}}univariate{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}{\isaliteral{22}{\isachardoublequote}}equation{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
3.445 +{\isaliteral{2A7D}{\isacharverbatimclose}}%
3.446 +\endisatagML
3.447 +{\isafoldML}%
3.448 +%
3.449 +\isadelimML
3.450 +%
3.451 +\endisadelimML
3.452 +%
3.453 +\begin{isamarkuptext}%
3.454 +Solve Equation Stepwise%
3.455 +\end{isamarkuptext}%
3.456 +\isamarkuptrue%
3.457 +%
3.458 +\isadelimML
3.459 +%
3.460 +\endisadelimML
3.461 +%
3.462 +\isatagML
3.463 +\isacommand{ML}\isamarkupfalse%
3.464 +\ {\isaliteral{7B2A}{\isacharverbatimopen}}\isanewline
3.465 +val\ {\isaliteral{28}{\isacharparenleft}}p{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}f{\isaliteral{2C}{\isacharcomma}}nxt{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}pt{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ CalcTreeTEST\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{28}{\isacharparenleft}}fmz{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{28}{\isacharparenleft}}dI{\isaliteral{27}{\isacharprime}}{\isaliteral{2C}{\isacharcomma}}pI{\isaliteral{27}{\isacharprime}}{\isaliteral{2C}{\isacharcomma}}mI{\isaliteral{27}{\isacharprime}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
3.466 +val\ {\isaliteral{28}{\isacharparenleft}}p{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}f{\isaliteral{2C}{\isacharcomma}}nxt{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}pt{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ me\ nxt\ p\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ pt{\isaliteral{3B}{\isacharsemicolon}}\isanewline
3.467 +val\ {\isaliteral{28}{\isacharparenleft}}p{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}f{\isaliteral{2C}{\isacharcomma}}nxt{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}pt{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ me\ nxt\ p\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ pt{\isaliteral{3B}{\isacharsemicolon}}\isanewline
3.468 +val\ {\isaliteral{28}{\isacharparenleft}}p{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}f{\isaliteral{2C}{\isacharcomma}}nxt{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}pt{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ me\ nxt\ p\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ pt{\isaliteral{3B}{\isacharsemicolon}}\isanewline
3.469 +val\ {\isaliteral{28}{\isacharparenleft}}p{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}f{\isaliteral{2C}{\isacharcomma}}nxt{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}pt{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ me\ nxt\ p\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ pt{\isaliteral{3B}{\isacharsemicolon}}\isanewline
3.470 +val\ {\isaliteral{28}{\isacharparenleft}}p{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}f{\isaliteral{2C}{\isacharcomma}}nxt{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}pt{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ me\ nxt\ p\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ pt{\isaliteral{3B}{\isacharsemicolon}}\isanewline
3.471 +val\ {\isaliteral{28}{\isacharparenleft}}p{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}f{\isaliteral{2C}{\isacharcomma}}nxt{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}pt{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ me\ nxt\ p\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ pt{\isaliteral{3B}{\isacharsemicolon}}\isanewline
3.472 +val\ {\isaliteral{28}{\isacharparenleft}}p{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}f{\isaliteral{2C}{\isacharcomma}}nxt{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}pt{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ me\ nxt\ p\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ pt{\isaliteral{3B}{\isacharsemicolon}}\isanewline
3.473 +val\ {\isaliteral{28}{\isacharparenleft}}p{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}f{\isaliteral{2C}{\isacharcomma}}nxt{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}pt{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ me\ nxt\ p\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ pt{\isaliteral{3B}{\isacharsemicolon}}\isanewline
3.474 +val\ {\isaliteral{28}{\isacharparenleft}}p{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}f{\isaliteral{2C}{\isacharcomma}}nxt{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}pt{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ me\ nxt\ p\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ pt{\isaliteral{3B}{\isacharsemicolon}}\isanewline
3.475 +val\ {\isaliteral{28}{\isacharparenleft}}p{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}f{\isaliteral{2C}{\isacharcomma}}nxt{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}pt{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ me\ nxt\ p\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ pt{\isaliteral{3B}{\isacharsemicolon}}\isanewline
3.476 +val\ {\isaliteral{28}{\isacharparenleft}}p{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}f{\isaliteral{2C}{\isacharcomma}}nxt{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}pt{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ me\ nxt\ p\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ pt{\isaliteral{3B}{\isacharsemicolon}}\ \ \ \ \ \ \ \ \ \isanewline
3.477 +val\ {\isaliteral{28}{\isacharparenleft}}p{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}f{\isaliteral{2C}{\isacharcomma}}nxt{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}pt{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ me\ nxt\ p\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ pt{\isaliteral{3B}{\isacharsemicolon}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{2A}{\isacharasterisk}}nxt\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}{\isaliteral{2C}{\isacharcomma}}Check{\isaliteral{5F}{\isacharunderscore}}elementwise\ {\isaliteral{22}{\isachardoublequote}}Assumptions{\isaliteral{22}{\isachardoublequote}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{29}{\isacharparenright}}\isanewline
3.478 +val\ {\isaliteral{28}{\isacharparenleft}}p{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}f{\isaliteral{2C}{\isacharcomma}}nxt{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}pt{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ me\ nxt\ p\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ pt{\isaliteral{3B}{\isacharsemicolon}}\ \ \ \ \ \ \ \ \ \isanewline
3.479 +val\ {\isaliteral{28}{\isacharparenleft}}p{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}f{\isaliteral{2C}{\isacharcomma}}nxt{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}pt{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ me\ nxt\ p\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ pt{\isaliteral{3B}{\isacharsemicolon}}\ f{\isadigit{2}}str\ f{\isaliteral{3B}{\isacharsemicolon}}\isanewline
3.480 +{\isaliteral{28}{\isacharparenleft}}{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{5B}{\isacharbrackleft}}z\ {\isaliteral{3D}{\isacharequal}}\ {\isadigit{1}}\ {\isaliteral{2F}{\isacharslash}}\ {\isadigit{8}}\ {\isaliteral{2B}{\isacharplus}}\ sqrt\ {\isaliteral{28}{\isacharparenleft}}{\isadigit{9}}\ {\isaliteral{2F}{\isacharslash}}\ {\isadigit{1}}{\isadigit{6}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{2F}{\isacharslash}}\ {\isadigit{2}}{\isaliteral{2C}{\isacharcomma}}\ z\ {\isaliteral{3D}{\isacharequal}}\ {\isadigit{1}}\ {\isaliteral{2F}{\isacharslash}}\ {\isadigit{8}}\ {\isaliteral{2B}{\isacharplus}}\ {\isaliteral{2D}{\isacharminus}}{\isadigit{1}}\ {\isaliteral{2A}{\isacharasterisk}}\ sqrt\ {\isaliteral{28}{\isacharparenleft}}{\isadigit{9}}\ {\isaliteral{2F}{\isacharslash}}\ {\isadigit{1}}{\isadigit{6}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{2F}{\isacharslash}}\ {\isadigit{2}}{\isaliteral{5D}{\isacharbrackright}}\ TODO\ sqrt{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{29}{\isacharparenright}}\isanewline
3.481 +show{\isaliteral{5F}{\isacharunderscore}}pt\ pt{\isaliteral{3B}{\isacharsemicolon}}\ \isanewline
3.482 +val\ SOME\ f\ {\isaliteral{3D}{\isacharequal}}\ parseNEW\ ctxt\ {\isaliteral{22}{\isachardoublequote}}{\isaliteral{5B}{\isacharbrackleft}}z{\isaliteral{3D}{\isacharequal}}{\isadigit{1}}{\isaliteral{2F}{\isacharslash}}{\isadigit{2}}{\isaliteral{2C}{\isacharcomma}}\ z{\isaliteral{3D}{\isacharequal}}{\isaliteral{2D}{\isacharminus}}{\isadigit{1}}{\isaliteral{2F}{\isacharslash}}{\isadigit{4}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
3.483 +{\isaliteral{2A7D}{\isacharverbatimclose}}%
3.484 +\endisatagML
3.485 +{\isafoldML}%
3.486 +%
3.487 +\isadelimML
3.488 +%
3.489 +\endisadelimML
3.490 +%
3.491 +\isamarkupsubsection{partial fraction decomposition%
3.492 +}
3.493 +\isamarkuptrue%
3.494 +%
3.495 +\isamarkupsubsubsection{solution of the equation%
3.496 +}
3.497 +\isamarkuptrue%
3.498 +%
3.499 +\isadelimML
3.500 +%
3.501 +\endisadelimML
3.502 +%
3.503 +\isatagML
3.504 +\isacommand{ML}\isamarkupfalse%
3.505 +\ {\isaliteral{7B2A}{\isacharverbatimopen}}\isanewline
3.506 +val\ SOME\ solutions\ {\isaliteral{3D}{\isacharequal}}\ parseNEW\ ctxt\ {\isaliteral{22}{\isachardoublequote}}{\isaliteral{5B}{\isacharbrackleft}}z{\isaliteral{3D}{\isacharequal}}{\isadigit{1}}{\isaliteral{2F}{\isacharslash}}{\isadigit{2}}{\isaliteral{2C}{\isacharcomma}}\ z{\isaliteral{3D}{\isacharequal}}{\isaliteral{2D}{\isacharminus}}{\isadigit{1}}{\isaliteral{2F}{\isacharslash}}{\isadigit{4}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
3.507 +term{\isadigit{2}}str\ solutions{\isaliteral{3B}{\isacharsemicolon}}\isanewline
3.508 +atomty\ solutions{\isaliteral{3B}{\isacharsemicolon}}\isanewline
3.509 +{\isaliteral{2A7D}{\isacharverbatimclose}}%
3.510 +\endisatagML
3.511 +{\isafoldML}%
3.512 +%
3.513 +\isadelimML
3.514 +%
3.515 +\endisadelimML
3.516 +%
3.517 +\isamarkupsubsubsection{get solutions out of list%
3.518 +}
3.519 +\isamarkuptrue%
3.520 +%
3.521 +\begin{isamarkuptext}%
3.522 +in isac's CTP-based programming language: let$ $s_1 = NTH 1$ solutions; $s_2 = NTH 2...$%
3.523 +\end{isamarkuptext}%
3.524 +\isamarkuptrue%
3.525 +%
3.526 +\isadelimML
3.527 +%
3.528 +\endisadelimML
3.529 +%
3.530 +\isatagML
3.531 +\isacommand{ML}\isamarkupfalse%
3.532 +\ {\isaliteral{7B2A}{\isacharverbatimopen}}\isanewline
3.533 +val\ Const\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{22}{\isachardoublequote}}List{\isaliteral{2E}{\isachardot}}list{\isaliteral{2E}{\isachardot}}Cons{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5F}{\isacharunderscore}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{24}{\isachardollar}}\ s{\isaliteral{5F}{\isacharunderscore}}{\isadigit{1}}\ {\isaliteral{24}{\isachardollar}}\ {\isaliteral{28}{\isacharparenleft}}Const\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{22}{\isachardoublequote}}List{\isaliteral{2E}{\isachardot}}list{\isaliteral{2E}{\isachardot}}Cons{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5F}{\isacharunderscore}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{24}{\isachardollar}}\isanewline
3.534 +\ \ \ \ \ \ s{\isaliteral{5F}{\isacharunderscore}}{\isadigit{2}}\ {\isaliteral{24}{\isachardollar}}\ Const\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{22}{\isachardoublequote}}List{\isaliteral{2E}{\isachardot}}list{\isaliteral{2E}{\isachardot}}Nil{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5F}{\isacharunderscore}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ solutions{\isaliteral{3B}{\isacharsemicolon}}\isanewline
3.535 +term{\isadigit{2}}str\ s{\isaliteral{5F}{\isacharunderscore}}{\isadigit{1}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
3.536 +term{\isadigit{2}}str\ s{\isaliteral{5F}{\isacharunderscore}}{\isadigit{2}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
3.537 +{\isaliteral{2A7D}{\isacharverbatimclose}}\isanewline
3.538 +\isanewline
3.539 +\isacommand{ML}\isamarkupfalse%
3.540 +\ {\isaliteral{7B2A}{\isacharverbatimopen}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{2A}{\isacharasterisk}}Solutions\ as\ Denominator\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ Denominator{\isadigit{1}}\ {\isaliteral{3D}{\isacharequal}}\ z\ {\isaliteral{2D}{\isacharminus}}\ Zeropoint{\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ Denominator{\isadigit{2}}\ {\isaliteral{3D}{\isacharequal}}\ z{\isaliteral{2D}{\isacharminus}}Zeropoint{\isadigit{2}}{\isaliteral{2C}{\isacharcomma}}{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{29}{\isacharparenright}}\isanewline
3.541 +val\ xx\ {\isaliteral{3D}{\isacharequal}}\ HOLogic{\isaliteral{2E}{\isachardot}}dest{\isaliteral{5F}{\isacharunderscore}}eq\ s{\isaliteral{5F}{\isacharunderscore}}{\isadigit{1}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
3.542 +val\ s{\isaliteral{5F}{\isacharunderscore}}{\isadigit{1}}{\isaliteral{27}{\isacharprime}}\ {\isaliteral{3D}{\isacharequal}}\ HOLogic{\isaliteral{2E}{\isachardot}}mk{\isaliteral{5F}{\isacharunderscore}}binop\ {\isaliteral{22}{\isachardoublequote}}Groups{\isaliteral{2E}{\isachardot}}minus{\isaliteral{5F}{\isacharunderscore}}class{\isaliteral{2E}{\isachardot}}minus{\isaliteral{22}{\isachardoublequote}}\ xx{\isaliteral{3B}{\isacharsemicolon}}\isanewline
3.543 +val\ xx\ {\isaliteral{3D}{\isacharequal}}\ HOLogic{\isaliteral{2E}{\isachardot}}dest{\isaliteral{5F}{\isacharunderscore}}eq\ s{\isaliteral{5F}{\isacharunderscore}}{\isadigit{2}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
3.544 +val\ s{\isaliteral{5F}{\isacharunderscore}}{\isadigit{2}}{\isaliteral{27}{\isacharprime}}\ {\isaliteral{3D}{\isacharequal}}\ HOLogic{\isaliteral{2E}{\isachardot}}mk{\isaliteral{5F}{\isacharunderscore}}binop\ {\isaliteral{22}{\isachardoublequote}}Groups{\isaliteral{2E}{\isachardot}}minus{\isaliteral{5F}{\isacharunderscore}}class{\isaliteral{2E}{\isachardot}}minus{\isaliteral{22}{\isachardoublequote}}\ xx{\isaliteral{3B}{\isacharsemicolon}}\isanewline
3.545 +term{\isadigit{2}}str\ s{\isaliteral{5F}{\isacharunderscore}}{\isadigit{1}}{\isaliteral{27}{\isacharprime}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
3.546 +term{\isadigit{2}}str\ s{\isaliteral{5F}{\isacharunderscore}}{\isadigit{2}}{\isaliteral{27}{\isacharprime}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
3.547 +{\isaliteral{2A7D}{\isacharverbatimclose}}%
3.548 +\endisatagML
3.549 +{\isafoldML}%
3.550 +%
3.551 +\isadelimML
3.552 +%
3.553 +\endisadelimML
3.554 +%
3.555 +\isamarkupsubsubsection{build expression%
3.556 +}
3.557 +\isamarkuptrue%
3.558 +%
3.559 +\begin{isamarkuptext}%
3.560 +in isac's CTP-based programming language: let s_1 = Take numerator / (s_1 * s_2)%
3.561 +\end{isamarkuptext}%
3.562 +\isamarkuptrue%
3.563 +%
3.564 +\isadelimML
3.565 +%
3.566 +\endisadelimML
3.567 +%
3.568 +\isatagML
3.569 +\isacommand{ML}\isamarkupfalse%
3.570 +\ {\isaliteral{7B2A}{\isacharverbatimopen}}\isanewline
3.571 +{\isaliteral{28}{\isacharparenleft}}{\isaliteral{2A}{\isacharasterisk}}The\ Main\ Denominator\ is\ the\ multiplikation\ of\ the\ partial\ fraction\ denominators{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{29}{\isacharparenright}}\isanewline
3.572 +val\ denominator{\isaliteral{27}{\isacharprime}}\ {\isaliteral{3D}{\isacharequal}}\ HOLogic{\isaliteral{2E}{\isachardot}}mk{\isaliteral{5F}{\isacharunderscore}}binop\ {\isaliteral{22}{\isachardoublequote}}Groups{\isaliteral{2E}{\isachardot}}times{\isaliteral{5F}{\isacharunderscore}}class{\isaliteral{2E}{\isachardot}}times{\isaliteral{22}{\isachardoublequote}}\ {\isaliteral{28}{\isacharparenleft}}s{\isaliteral{5F}{\isacharunderscore}}{\isadigit{1}}{\isaliteral{27}{\isacharprime}}{\isaliteral{2C}{\isacharcomma}}\ s{\isaliteral{5F}{\isacharunderscore}}{\isadigit{2}}{\isaliteral{27}{\isacharprime}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3B}{\isacharsemicolon}}\isanewline
3.573 +val\ SOME\ numerator\ {\isaliteral{3D}{\isacharequal}}\ parseNEW\ ctxt\ {\isaliteral{22}{\isachardoublequote}}{\isadigit{3}}{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}real{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
3.574 +\isanewline
3.575 +val\ expr{\isaliteral{27}{\isacharprime}}\ {\isaliteral{3D}{\isacharequal}}\ HOLogic{\isaliteral{2E}{\isachardot}}mk{\isaliteral{5F}{\isacharunderscore}}binop\ {\isaliteral{22}{\isachardoublequote}}Rings{\isaliteral{2E}{\isachardot}}inverse{\isaliteral{5F}{\isacharunderscore}}class{\isaliteral{2E}{\isachardot}}divide{\isaliteral{22}{\isachardoublequote}}\ {\isaliteral{28}{\isacharparenleft}}numerator{\isaliteral{2C}{\isacharcomma}}\ denominator{\isaliteral{27}{\isacharprime}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
3.576 +term{\isadigit{2}}str\ expr{\isaliteral{27}{\isacharprime}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
3.577 +{\isaliteral{2A7D}{\isacharverbatimclose}}%
3.578 +\endisatagML
3.579 +{\isafoldML}%
3.580 +%
3.581 +\isadelimML
3.582 +%
3.583 +\endisadelimML
3.584 +%
3.585 +\isamarkupsubsubsection{Ansatz - create partial fractions out of our expression%
3.586 +}
3.587 +\isamarkuptrue%
3.588 +%
3.589 +\isadelimML
3.590 +%
3.591 +\endisadelimML
3.592 +%
3.593 +\isatagML
3.594 +\isacommand{ML}\isamarkupfalse%
3.595 +\ {\isaliteral{7B2A}{\isacharverbatimopen}}Context{\isaliteral{2E}{\isachardot}}theory{\isaliteral{5F}{\isacharunderscore}}name\ thy\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{22}{\isachardoublequote}}Isac{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{2A7D}{\isacharverbatimclose}}%
3.596 +\endisatagML
3.597 +{\isafoldML}%
3.598 +%
3.599 +\isadelimML
3.600 +%
3.601 +\endisadelimML
3.602 +\isanewline
3.603 +\isanewline
3.604 +\isacommand{axiomatization}\isamarkupfalse%
3.605 +\ \isakeyword{where}\isanewline
3.606 +\ \ ansatz{\isadigit{2}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}n\ {\isaliteral{2F}{\isacharslash}}\ {\isaliteral{28}{\isacharparenleft}}a{\isaliteral{2A}{\isacharasterisk}}b{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ A{\isaliteral{2F}{\isacharslash}}a\ {\isaliteral{2B}{\isacharplus}}\ B{\isaliteral{2F}{\isacharslash}}{\isaliteral{28}{\isacharparenleft}}b{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}real{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\ \isakeyword{and}\isanewline
3.607 +\ \ multiply{\isaliteral{5F}{\isacharunderscore}}eq{\isadigit{2}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{28}{\isacharparenleft}}n\ {\isaliteral{2F}{\isacharslash}}\ {\isaliteral{28}{\isacharparenleft}}a{\isaliteral{2A}{\isacharasterisk}}b{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ A{\isaliteral{2F}{\isacharslash}}a\ {\isaliteral{2B}{\isacharplus}}\ B{\isaliteral{2F}{\isacharslash}}b{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}a{\isaliteral{2A}{\isacharasterisk}}b{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{28}{\isacharparenleft}}n\ \ {\isaliteral{2F}{\isacharslash}}\ {\isaliteral{28}{\isacharparenleft}}a{\isaliteral{2A}{\isacharasterisk}}b{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ a{\isaliteral{2A}{\isacharasterisk}}b{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{28}{\isacharparenleft}}A{\isaliteral{2F}{\isacharslash}}a\ {\isaliteral{2B}{\isacharplus}}\ B{\isaliteral{2F}{\isacharslash}}b{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
3.608 +%
3.609 +\isadelimML
3.610 +\isanewline
3.611 +%
3.612 +\endisadelimML
3.613 +%
3.614 +\isatagML
3.615 +\isacommand{ML}\isamarkupfalse%
3.616 +\ {\isaliteral{7B2A}{\isacharverbatimopen}}\isanewline
3.617 +{\isaliteral{28}{\isacharparenleft}}{\isaliteral{2A}{\isacharasterisk}}we\ use\ our\ ansatz{\isadigit{2}}\ to\ rewrite\ our\ expression\ and\ get\ an\ equilation\ with\ our\ expression\ on\ the\ left\ and\ the\ partial\ fractions\ of\ it\ on\ the\ right\ side{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{29}{\isacharparenright}}\isanewline
3.618 +val\ SOME\ {\isaliteral{28}{\isacharparenleft}}t{\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ rewrite{\isaliteral{5F}{\isacharunderscore}}\ %
3.619 +\isaantiq
3.620 +theory\ Isac{}%
3.621 +\endisaantiq
3.622 +\ e{\isaliteral{5F}{\isacharunderscore}}rew{\isaliteral{5F}{\isacharunderscore}}ord\ e{\isaliteral{5F}{\isacharunderscore}}rls\ false\ %
3.623 +\isaantiq
3.624 +thm\ ansatz{\isadigit{2}}{}%
3.625 +\endisaantiq
3.626 +\ expr{\isaliteral{27}{\isacharprime}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
3.627 +term{\isadigit{2}}str\ t{\isadigit{1}}{\isaliteral{3B}{\isacharsemicolon}}\ atomty\ t{\isadigit{1}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
3.628 +val\ eq{\isadigit{1}}\ {\isaliteral{3D}{\isacharequal}}\ HOLogic{\isaliteral{2E}{\isachardot}}mk{\isaliteral{5F}{\isacharunderscore}}eq\ {\isaliteral{28}{\isacharparenleft}}expr{\isaliteral{27}{\isacharprime}}{\isaliteral{2C}{\isacharcomma}}\ t{\isadigit{1}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
3.629 +term{\isadigit{2}}str\ eq{\isadigit{1}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
3.630 +{\isaliteral{2A7D}{\isacharverbatimclose}}\isanewline
3.631 +\isacommand{ML}\isamarkupfalse%
3.632 +\ {\isaliteral{7B2A}{\isacharverbatimopen}}\isanewline
3.633 +{\isaliteral{28}{\isacharparenleft}}{\isaliteral{2A}{\isacharasterisk}}eliminate\ the\ demoninators\ by\ multiplying\ the\ left\ and\ the\ right\ side\ with\ the\ main\ denominator{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{29}{\isacharparenright}}\isanewline
3.634 +val\ SOME\ {\isaliteral{28}{\isacharparenleft}}eq{\isadigit{2}}{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ rewrite{\isaliteral{5F}{\isacharunderscore}}\ %
3.635 +\isaantiq
3.636 +theory\ Isac{}%
3.637 +\endisaantiq
3.638 +\ e{\isaliteral{5F}{\isacharunderscore}}rew{\isaliteral{5F}{\isacharunderscore}}ord\ e{\isaliteral{5F}{\isacharunderscore}}rls\ false\ %
3.639 +\isaantiq
3.640 +thm\ multiply{\isaliteral{5F}{\isacharunderscore}}eq{\isadigit{2}}{}%
3.641 +\endisaantiq
3.642 +\ eq{\isadigit{1}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
3.643 +term{\isadigit{2}}str\ eq{\isadigit{2}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
3.644 +{\isaliteral{2A7D}{\isacharverbatimclose}}\isanewline
3.645 +\isacommand{ML}\isamarkupfalse%
3.646 +\ {\isaliteral{7B2A}{\isacharverbatimopen}}\isanewline
3.647 +{\isaliteral{28}{\isacharparenleft}}{\isaliteral{2A}{\isacharasterisk}}simplificatoin{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{29}{\isacharparenright}}\isanewline
3.648 +val\ SOME\ {\isaliteral{28}{\isacharparenleft}}eq{\isadigit{3}}{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ rewrite{\isaliteral{5F}{\isacharunderscore}}set{\isaliteral{5F}{\isacharunderscore}}\ %
3.649 +\isaantiq
3.650 +theory\ Isac{}%
3.651 +\endisaantiq
3.652 +\ false\ norm{\isaliteral{5F}{\isacharunderscore}}Rational\ eq{\isadigit{2}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
3.653 +term{\isadigit{2}}str\ eq{\isadigit{3}}{\isaliteral{3B}{\isacharsemicolon}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{3F}{\isacharquery}}A\ {\isaliteral{3F}{\isacharquery}}B\ not\ simplified{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{29}{\isacharparenright}}\isanewline
3.654 +{\isaliteral{2A7D}{\isacharverbatimclose}}\isanewline
3.655 +\isacommand{ML}\isamarkupfalse%
3.656 +\ {\isaliteral{7B2A}{\isacharverbatimopen}}\isanewline
3.657 +val\ SOME\ fract{\isadigit{1}}\ {\isaliteral{3D}{\isacharequal}}\isanewline
3.658 +\ \ parseNEW\ ctxt\ {\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}z\ {\isaliteral{2D}{\isacharminus}}\ {\isadigit{1}}\ {\isaliteral{2F}{\isacharslash}}\ {\isadigit{2}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{2A}{\isacharasterisk}}\ {\isaliteral{28}{\isacharparenleft}}z\ {\isaliteral{2D}{\isacharminus}}\ {\isaliteral{2D}{\isacharminus}}{\isadigit{1}}\ {\isaliteral{2F}{\isacharslash}}\ {\isadigit{4}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{2A}{\isacharasterisk}}\ {\isaliteral{28}{\isacharparenleft}}A\ {\isaliteral{2F}{\isacharslash}}\ {\isaliteral{28}{\isacharparenleft}}z\ {\isaliteral{2D}{\isacharminus}}\ {\isadigit{1}}\ {\isaliteral{2F}{\isacharslash}}\ {\isadigit{2}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{2B}{\isacharplus}}\ B\ {\isaliteral{2F}{\isacharslash}}\ {\isaliteral{28}{\isacharparenleft}}z\ {\isaliteral{2D}{\isacharminus}}\ {\isaliteral{2D}{\isacharminus}}{\isadigit{1}}\ {\isaliteral{2F}{\isacharslash}}\ {\isadigit{4}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3B}{\isacharsemicolon}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{2A}{\isacharasterisk}}A\ B\ {\isaliteral{21}{\isacharbang}}{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{29}{\isacharparenright}}\isanewline
3.659 +val\ SOME\ {\isaliteral{28}{\isacharparenleft}}fract{\isadigit{2}}{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ rewrite{\isaliteral{5F}{\isacharunderscore}}set{\isaliteral{5F}{\isacharunderscore}}\ %
3.660 +\isaantiq
3.661 +theory\ Isac{}%
3.662 +\endisaantiq
3.663 +\ false\ norm{\isaliteral{5F}{\isacharunderscore}}Rational\ fract{\isadigit{1}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
3.664 +term{\isadigit{2}}str\ fract{\isadigit{2}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}A\ {\isaliteral{2B}{\isacharplus}}\ {\isaliteral{2D}{\isacharminus}}{\isadigit{2}}\ {\isaliteral{2A}{\isacharasterisk}}\ B\ {\isaliteral{2B}{\isacharplus}}\ {\isadigit{4}}\ {\isaliteral{2A}{\isacharasterisk}}\ A\ {\isaliteral{2A}{\isacharasterisk}}\ z\ {\isaliteral{2B}{\isacharplus}}\ {\isadigit{4}}\ {\isaliteral{2A}{\isacharasterisk}}\ B\ {\isaliteral{2A}{\isacharasterisk}}\ z{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{2F}{\isacharslash}}\ {\isadigit{4}}{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
3.665 +{\isaliteral{28}{\isacharparenleft}}{\isaliteral{2A}{\isacharasterisk}}term{\isadigit{2}}str\ fract{\isadigit{2}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{22}{\isachardoublequote}}A\ {\isaliteral{2A}{\isacharasterisk}}\ {\isaliteral{28}{\isacharparenleft}}{\isadigit{1}}\ {\isaliteral{2F}{\isacharslash}}\ {\isadigit{4}}\ {\isaliteral{2B}{\isacharplus}}\ z{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{2B}{\isacharplus}}\ B\ {\isaliteral{2A}{\isacharasterisk}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{2D}{\isacharminus}}{\isadigit{1}}\ {\isaliteral{2F}{\isacharslash}}\ {\isadigit{2}}\ {\isaliteral{2B}{\isacharplus}}\ z{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}\ would\ be\ more\ traditional{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{29}{\isacharparenright}}\isanewline
3.666 +{\isaliteral{2A7D}{\isacharverbatimclose}}\isanewline
3.667 +\isacommand{ML}\isamarkupfalse%
3.668 +\ {\isaliteral{7B2A}{\isacharverbatimopen}}\isanewline
3.669 +val\ {\isaliteral{28}{\isacharparenleft}}numerator{\isaliteral{2C}{\isacharcomma}}\ denominator{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ HOLogic{\isaliteral{2E}{\isachardot}}dest{\isaliteral{5F}{\isacharunderscore}}eq\ eq{\isadigit{3}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
3.670 +val\ eq{\isadigit{3}}{\isaliteral{27}{\isacharprime}}\ {\isaliteral{3D}{\isacharequal}}\ HOLogic{\isaliteral{2E}{\isachardot}}mk{\isaliteral{5F}{\isacharunderscore}}eq\ {\isaliteral{28}{\isacharparenleft}}numerator{\isaliteral{2C}{\isacharcomma}}\ fract{\isadigit{1}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{3B}{\isacharsemicolon}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{2A}{\isacharasterisk}}A\ B\ {\isaliteral{21}{\isacharbang}}{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{29}{\isacharparenright}}\isanewline
3.671 +term{\isadigit{2}}str\ eq{\isadigit{3}}{\isaliteral{27}{\isacharprime}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
3.672 +{\isaliteral{28}{\isacharparenleft}}{\isaliteral{2A}{\isacharasterisk}}MANDATORY{\isaliteral{3A}{\isacharcolon}}\ simplify\ {\isaliteral{28}{\isacharparenleft}}and\ remove\ denominator{\isaliteral{29}{\isacharparenright}}\ otherwise\ {\isadigit{3}}\ {\isaliteral{3D}{\isacharequal}}\ {\isadigit{0}}{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{29}{\isacharparenright}}\isanewline
3.673 +val\ SOME\ {\isaliteral{28}{\isacharparenleft}}eq{\isadigit{3}}{\isaliteral{27}{\isacharprime}}{\isaliteral{27}{\isacharprime}}\ {\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ rewrite{\isaliteral{5F}{\isacharunderscore}}set{\isaliteral{5F}{\isacharunderscore}}\ %
3.674 +\isaantiq
3.675 +theory\ Isac{}%
3.676 +\endisaantiq
3.677 +\ false\ norm{\isaliteral{5F}{\isacharunderscore}}Rational\ eq{\isadigit{3}}{\isaliteral{27}{\isacharprime}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
3.678 +term{\isadigit{2}}str\ eq{\isadigit{3}}{\isaliteral{27}{\isacharprime}}{\isaliteral{27}{\isacharprime}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
3.679 +{\isaliteral{2A7D}{\isacharverbatimclose}}\isanewline
3.680 +\isacommand{ML}\isamarkupfalse%
3.681 +\ {\isaliteral{7B2A}{\isacharverbatimopen}}Context{\isaliteral{2E}{\isachardot}}theory{\isaliteral{5F}{\isacharunderscore}}name\ thy\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{22}{\isachardoublequote}}Isac{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{2A7D}{\isacharverbatimclose}}%
3.682 +\endisatagML
3.683 +{\isafoldML}%
3.684 +%
3.685 +\isadelimML
3.686 +%
3.687 +\endisadelimML
3.688 +%
3.689 +\isamarkupsubsubsection{get first koeffizient%
3.690 +}
3.691 +\isamarkuptrue%
3.692 +%
3.693 +\isadelimML
3.694 +%
3.695 +\endisadelimML
3.696 +%
3.697 +\isatagML
3.698 +\isacommand{ML}\isamarkupfalse%
3.699 +\ {\isaliteral{7B2A}{\isacharverbatimopen}}\isanewline
3.700 +{\isaliteral{28}{\isacharparenleft}}{\isaliteral{2A}{\isacharasterisk}}substitude\ z\ with\ the\ first\ zeropoint\ to\ get\ A{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{29}{\isacharparenright}}\isanewline
3.701 +val\ SOME\ {\isaliteral{28}{\isacharparenleft}}eq{\isadigit{4}}{\isaliteral{5F}{\isacharunderscore}}{\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ rewrite{\isaliteral{5F}{\isacharunderscore}}terms{\isaliteral{5F}{\isacharunderscore}}\ %
3.702 +\isaantiq
3.703 +theory\ Isac{}%
3.704 +\endisaantiq
3.705 +\ e{\isaliteral{5F}{\isacharunderscore}}rew{\isaliteral{5F}{\isacharunderscore}}ord\ e{\isaliteral{5F}{\isacharunderscore}}rls\ {\isaliteral{5B}{\isacharbrackleft}}s{\isaliteral{5F}{\isacharunderscore}}{\isadigit{1}}{\isaliteral{5D}{\isacharbrackright}}\ eq{\isadigit{3}}{\isaliteral{27}{\isacharprime}}{\isaliteral{27}{\isacharprime}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
3.706 +term{\isadigit{2}}str\ eq{\isadigit{4}}{\isaliteral{5F}{\isacharunderscore}}{\isadigit{1}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
3.707 +\isanewline
3.708 +val\ SOME\ {\isaliteral{28}{\isacharparenleft}}eq{\isadigit{4}}{\isaliteral{5F}{\isacharunderscore}}{\isadigit{2}}{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ rewrite{\isaliteral{5F}{\isacharunderscore}}set{\isaliteral{5F}{\isacharunderscore}}\ %
3.709 +\isaantiq
3.710 +theory\ Isac{}%
3.711 +\endisaantiq
3.712 +\ false\ norm{\isaliteral{5F}{\isacharunderscore}}Rational\ eq{\isadigit{4}}{\isaliteral{5F}{\isacharunderscore}}{\isadigit{1}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
3.713 +term{\isadigit{2}}str\ eq{\isadigit{4}}{\isaliteral{5F}{\isacharunderscore}}{\isadigit{2}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
3.714 +\isanewline
3.715 +val\ fmz\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{22}{\isachardoublequote}}equality\ {\isaliteral{28}{\isacharparenleft}}{\isadigit{3}}\ {\isaliteral{3D}{\isacharequal}}\ {\isadigit{3}}\ {\isaliteral{2A}{\isacharasterisk}}\ A\ {\isaliteral{2F}{\isacharslash}}\ {\isaliteral{28}{\isacharparenleft}}{\isadigit{4}}{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}real{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{22}{\isachardoublequote}}solveFor\ A{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}{\isaliteral{22}{\isachardoublequote}}solutions\ L{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
3.716 +val\ {\isaliteral{28}{\isacharparenleft}}dI{\isaliteral{27}{\isacharprime}}{\isaliteral{2C}{\isacharcomma}}pI{\isaliteral{27}{\isacharprime}}{\isaliteral{2C}{\isacharcomma}}mI{\isaliteral{27}{\isacharprime}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{22}{\isachardoublequote}}Isac{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{22}{\isachardoublequote}}univariate{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}{\isaliteral{22}{\isachardoublequote}}equation{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{22}{\isachardoublequote}}no{\isaliteral{5F}{\isacharunderscore}}met{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
3.717 +{\isaliteral{28}{\isacharparenleft}}{\isaliteral{2A}{\isacharasterisk}}solve\ the\ simple\ linear\ equilation\ for\ A\ TODO{\isaliteral{3A}{\isacharcolon}}\ return\ eq{\isaliteral{2C}{\isacharcomma}}\ not\ list\ of\ eq{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{29}{\isacharparenright}}\isanewline
3.718 +val\ {\isaliteral{28}{\isacharparenleft}}p{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}fa{\isaliteral{2C}{\isacharcomma}}nxt{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}pt{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ CalcTreeTEST\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{28}{\isacharparenleft}}fmz{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{28}{\isacharparenleft}}dI{\isaliteral{27}{\isacharprime}}{\isaliteral{2C}{\isacharcomma}}pI{\isaliteral{27}{\isacharprime}}{\isaliteral{2C}{\isacharcomma}}mI{\isaliteral{27}{\isacharprime}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
3.719 +val\ {\isaliteral{28}{\isacharparenleft}}p{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}fa{\isaliteral{2C}{\isacharcomma}}nxt{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}pt{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ me\ nxt\ p\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ pt{\isaliteral{3B}{\isacharsemicolon}}\isanewline
3.720 +val\ {\isaliteral{28}{\isacharparenleft}}p{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}fa{\isaliteral{2C}{\isacharcomma}}nxt{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}pt{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ me\ nxt\ p\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ pt{\isaliteral{3B}{\isacharsemicolon}}\isanewline
3.721 +val\ {\isaliteral{28}{\isacharparenleft}}p{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}fa{\isaliteral{2C}{\isacharcomma}}nxt{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}pt{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ me\ nxt\ p\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ pt{\isaliteral{3B}{\isacharsemicolon}}\isanewline
3.722 +val\ {\isaliteral{28}{\isacharparenleft}}p{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}fa{\isaliteral{2C}{\isacharcomma}}nxt{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}pt{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ me\ nxt\ p\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ pt{\isaliteral{3B}{\isacharsemicolon}}\isanewline
3.723 +val\ {\isaliteral{28}{\isacharparenleft}}p{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}fa{\isaliteral{2C}{\isacharcomma}}nxt{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}pt{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ me\ nxt\ p\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ pt{\isaliteral{3B}{\isacharsemicolon}}\isanewline
3.724 +val\ {\isaliteral{28}{\isacharparenleft}}p{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}fa{\isaliteral{2C}{\isacharcomma}}nxt{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}pt{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ me\ nxt\ p\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ pt{\isaliteral{3B}{\isacharsemicolon}}\isanewline
3.725 +val\ {\isaliteral{28}{\isacharparenleft}}p{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}fa{\isaliteral{2C}{\isacharcomma}}nxt{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}pt{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ me\ nxt\ p\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ pt{\isaliteral{3B}{\isacharsemicolon}}\isanewline
3.726 +val\ {\isaliteral{28}{\isacharparenleft}}p{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}fa{\isaliteral{2C}{\isacharcomma}}nxt{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}pt{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ me\ nxt\ p\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ pt{\isaliteral{3B}{\isacharsemicolon}}\isanewline
3.727 +val\ {\isaliteral{28}{\isacharparenleft}}p{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}fa{\isaliteral{2C}{\isacharcomma}}nxt{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}pt{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ me\ nxt\ p\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ pt{\isaliteral{3B}{\isacharsemicolon}}\isanewline
3.728 +val\ {\isaliteral{28}{\isacharparenleft}}p{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}fa{\isaliteral{2C}{\isacharcomma}}nxt{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}pt{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ me\ nxt\ p\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ pt{\isaliteral{3B}{\isacharsemicolon}}\isanewline
3.729 +val\ {\isaliteral{28}{\isacharparenleft}}p{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}fa{\isaliteral{2C}{\isacharcomma}}nxt{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}pt{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ me\ nxt\ p\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ pt{\isaliteral{3B}{\isacharsemicolon}}\isanewline
3.730 +val\ {\isaliteral{28}{\isacharparenleft}}p{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}fa{\isaliteral{2C}{\isacharcomma}}nxt{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}pt{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ me\ nxt\ p\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ pt{\isaliteral{3B}{\isacharsemicolon}}\isanewline
3.731 +val\ {\isaliteral{28}{\isacharparenleft}}p{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}fa{\isaliteral{2C}{\isacharcomma}}nxt{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}pt{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ me\ nxt\ p\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ pt{\isaliteral{3B}{\isacharsemicolon}}\isanewline
3.732 +val\ {\isaliteral{28}{\isacharparenleft}}p{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}fa{\isaliteral{2C}{\isacharcomma}}nxt{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}pt{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ me\ nxt\ p\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ pt{\isaliteral{3B}{\isacharsemicolon}}\isanewline
3.733 +val\ {\isaliteral{28}{\isacharparenleft}}p{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}fa{\isaliteral{2C}{\isacharcomma}}nxt{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}pt{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ me\ nxt\ p\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ pt{\isaliteral{3B}{\isacharsemicolon}}\isanewline
3.734 +val\ {\isaliteral{28}{\isacharparenleft}}p{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}fa{\isaliteral{2C}{\isacharcomma}}nxt{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}pt{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ me\ nxt\ p\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ pt{\isaliteral{3B}{\isacharsemicolon}}\isanewline
3.735 +val\ {\isaliteral{28}{\isacharparenleft}}p{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}fa{\isaliteral{2C}{\isacharcomma}}nxt{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}pt{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ me\ nxt\ p\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ pt{\isaliteral{3B}{\isacharsemicolon}}\isanewline
3.736 +val\ {\isaliteral{28}{\isacharparenleft}}p{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}fa{\isaliteral{2C}{\isacharcomma}}nxt{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}pt{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ me\ nxt\ p\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ pt{\isaliteral{3B}{\isacharsemicolon}}\isanewline
3.737 +val\ {\isaliteral{28}{\isacharparenleft}}p{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}fa{\isaliteral{2C}{\isacharcomma}}nxt{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}pt{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ me\ nxt\ p\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ pt{\isaliteral{3B}{\isacharsemicolon}}\isanewline
3.738 +val\ {\isaliteral{28}{\isacharparenleft}}p{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}fa{\isaliteral{2C}{\isacharcomma}}nxt{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}pt{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ me\ nxt\ p\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ pt{\isaliteral{3B}{\isacharsemicolon}}\isanewline
3.739 +val\ {\isaliteral{28}{\isacharparenleft}}p{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}fa{\isaliteral{2C}{\isacharcomma}}nxt{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}pt{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ me\ nxt\ p\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ pt{\isaliteral{3B}{\isacharsemicolon}}\isanewline
3.740 +val\ {\isaliteral{28}{\isacharparenleft}}p{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}fa{\isaliteral{2C}{\isacharcomma}}nxt{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}pt{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ me\ nxt\ p\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ pt{\isaliteral{3B}{\isacharsemicolon}}\isanewline
3.741 +val\ {\isaliteral{28}{\isacharparenleft}}p{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}fa{\isaliteral{2C}{\isacharcomma}}nxt{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}pt{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ me\ nxt\ p\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ pt{\isaliteral{3B}{\isacharsemicolon}}\isanewline
3.742 +val\ {\isaliteral{28}{\isacharparenleft}}p{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}fa{\isaliteral{2C}{\isacharcomma}}nxt{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}pt{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ me\ nxt\ p\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ pt{\isaliteral{3B}{\isacharsemicolon}}\isanewline
3.743 +val\ {\isaliteral{28}{\isacharparenleft}}p{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}fa{\isaliteral{2C}{\isacharcomma}}nxt{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}pt{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ me\ nxt\ p\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ pt{\isaliteral{3B}{\isacharsemicolon}}\isanewline
3.744 +val\ {\isaliteral{28}{\isacharparenleft}}p{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}fa{\isaliteral{2C}{\isacharcomma}}nxt{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}pt{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ me\ nxt\ p\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ pt{\isaliteral{3B}{\isacharsemicolon}}\isanewline
3.745 +val\ {\isaliteral{28}{\isacharparenleft}}p{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}fa{\isaliteral{2C}{\isacharcomma}}nxt{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}pt{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ me\ nxt\ p\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ pt{\isaliteral{3B}{\isacharsemicolon}}\ \isanewline
3.746 +f{\isadigit{2}}str\ fa{\isaliteral{3B}{\isacharsemicolon}}\isanewline
3.747 +{\isaliteral{2A7D}{\isacharverbatimclose}}%
3.748 +\endisatagML
3.749 +{\isafoldML}%
3.750 +%
3.751 +\isadelimML
3.752 +%
3.753 +\endisadelimML
3.754 +%
3.755 +\isamarkupsubsubsection{get second koeffizient%
3.756 +}
3.757 +\isamarkuptrue%
3.758 +%
3.759 +\isadelimML
3.760 +%
3.761 +\endisadelimML
3.762 +%
3.763 +\isatagML
3.764 +\isacommand{ML}\isamarkupfalse%
3.765 +\ {\isaliteral{7B2A}{\isacharverbatimopen}}thy{\isaliteral{2A7D}{\isacharverbatimclose}}\isanewline
3.766 +\isanewline
3.767 +\isacommand{ML}\isamarkupfalse%
3.768 +\ {\isaliteral{7B2A}{\isacharverbatimopen}}\isanewline
3.769 +{\isaliteral{28}{\isacharparenleft}}{\isaliteral{2A}{\isacharasterisk}}substitude\ z\ with\ the\ second\ zeropoint\ to\ get\ B{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{29}{\isacharparenright}}\isanewline
3.770 +val\ SOME\ {\isaliteral{28}{\isacharparenleft}}eq{\isadigit{4}}b{\isaliteral{5F}{\isacharunderscore}}{\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ rewrite{\isaliteral{5F}{\isacharunderscore}}terms{\isaliteral{5F}{\isacharunderscore}}\ %
3.771 +\isaantiq
3.772 +theory\ Isac{}%
3.773 +\endisaantiq
3.774 +\ e{\isaliteral{5F}{\isacharunderscore}}rew{\isaliteral{5F}{\isacharunderscore}}ord\ e{\isaliteral{5F}{\isacharunderscore}}rls\ {\isaliteral{5B}{\isacharbrackleft}}s{\isaliteral{5F}{\isacharunderscore}}{\isadigit{2}}{\isaliteral{5D}{\isacharbrackright}}\ eq{\isadigit{3}}{\isaliteral{27}{\isacharprime}}{\isaliteral{27}{\isacharprime}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
3.775 +term{\isadigit{2}}str\ eq{\isadigit{4}}b{\isaliteral{5F}{\isacharunderscore}}{\isadigit{1}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
3.776 +\isanewline
3.777 +val\ SOME\ {\isaliteral{28}{\isacharparenleft}}eq{\isadigit{4}}b{\isaliteral{5F}{\isacharunderscore}}{\isadigit{2}}{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ rewrite{\isaliteral{5F}{\isacharunderscore}}set{\isaliteral{5F}{\isacharunderscore}}\ %
3.778 +\isaantiq
3.779 +theory\ Isac{}%
3.780 +\endisaantiq
3.781 +\ false\ norm{\isaliteral{5F}{\isacharunderscore}}Rational\ eq{\isadigit{4}}b{\isaliteral{5F}{\isacharunderscore}}{\isadigit{1}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
3.782 +term{\isadigit{2}}str\ eq{\isadigit{4}}b{\isaliteral{5F}{\isacharunderscore}}{\isadigit{2}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
3.783 +{\isaliteral{2A7D}{\isacharverbatimclose}}\isanewline
3.784 +\isacommand{ML}\isamarkupfalse%
3.785 +\ {\isaliteral{7B2A}{\isacharverbatimopen}}\isanewline
3.786 +{\isaliteral{28}{\isacharparenleft}}{\isaliteral{2A}{\isacharasterisk}}solve\ the\ simple\ linear\ equilation\ for\ B\ TODO{\isaliteral{3A}{\isacharcolon}}\ return\ eq{\isaliteral{2C}{\isacharcomma}}\ not\ list\ of\ eq{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{29}{\isacharparenright}}\isanewline
3.787 +val\ fmz\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{22}{\isachardoublequote}}equality\ {\isaliteral{28}{\isacharparenleft}}{\isadigit{3}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{2D}{\isacharminus}}{\isadigit{3}}\ {\isaliteral{2A}{\isacharasterisk}}\ B\ {\isaliteral{2F}{\isacharslash}}\ {\isaliteral{28}{\isacharparenleft}}{\isadigit{4}}{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}real{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{22}{\isachardoublequote}}solveFor\ B{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}{\isaliteral{22}{\isachardoublequote}}solutions\ L{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
3.788 +val\ {\isaliteral{28}{\isacharparenleft}}dI{\isaliteral{27}{\isacharprime}}{\isaliteral{2C}{\isacharcomma}}pI{\isaliteral{27}{\isacharprime}}{\isaliteral{2C}{\isacharcomma}}mI{\isaliteral{27}{\isacharprime}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{22}{\isachardoublequote}}Isac{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{22}{\isachardoublequote}}univariate{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}{\isaliteral{22}{\isachardoublequote}}equation{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{22}{\isachardoublequote}}no{\isaliteral{5F}{\isacharunderscore}}met{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
3.789 +val\ {\isaliteral{28}{\isacharparenleft}}p{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}fb{\isaliteral{2C}{\isacharcomma}}nxt{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}pt{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ CalcTreeTEST\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{28}{\isacharparenleft}}fmz{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{28}{\isacharparenleft}}dI{\isaliteral{27}{\isacharprime}}{\isaliteral{2C}{\isacharcomma}}pI{\isaliteral{27}{\isacharprime}}{\isaliteral{2C}{\isacharcomma}}mI{\isaliteral{27}{\isacharprime}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
3.790 +val\ {\isaliteral{28}{\isacharparenleft}}p{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}fb{\isaliteral{2C}{\isacharcomma}}nxt{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}pt{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ me\ nxt\ p\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ pt{\isaliteral{3B}{\isacharsemicolon}}\isanewline
3.791 +val\ {\isaliteral{28}{\isacharparenleft}}p{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}fb{\isaliteral{2C}{\isacharcomma}}nxt{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}pt{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ me\ nxt\ p\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ pt{\isaliteral{3B}{\isacharsemicolon}}\isanewline
3.792 +val\ {\isaliteral{28}{\isacharparenleft}}p{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}fb{\isaliteral{2C}{\isacharcomma}}nxt{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}pt{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ me\ nxt\ p\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ pt{\isaliteral{3B}{\isacharsemicolon}}\isanewline
3.793 +val\ {\isaliteral{28}{\isacharparenleft}}p{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}fb{\isaliteral{2C}{\isacharcomma}}nxt{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}pt{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ me\ nxt\ p\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ pt{\isaliteral{3B}{\isacharsemicolon}}\isanewline
3.794 +val\ {\isaliteral{28}{\isacharparenleft}}p{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}fb{\isaliteral{2C}{\isacharcomma}}nxt{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}pt{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ me\ nxt\ p\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ pt{\isaliteral{3B}{\isacharsemicolon}}\isanewline
3.795 +val\ {\isaliteral{28}{\isacharparenleft}}p{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}fb{\isaliteral{2C}{\isacharcomma}}nxt{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}pt{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ me\ nxt\ p\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ pt{\isaliteral{3B}{\isacharsemicolon}}\isanewline
3.796 +val\ {\isaliteral{28}{\isacharparenleft}}p{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}fb{\isaliteral{2C}{\isacharcomma}}nxt{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}pt{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ me\ nxt\ p\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ pt{\isaliteral{3B}{\isacharsemicolon}}\isanewline
3.797 +val\ {\isaliteral{28}{\isacharparenleft}}p{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}fb{\isaliteral{2C}{\isacharcomma}}nxt{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}pt{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ me\ nxt\ p\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ pt{\isaliteral{3B}{\isacharsemicolon}}\isanewline
3.798 +val\ {\isaliteral{28}{\isacharparenleft}}p{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}fb{\isaliteral{2C}{\isacharcomma}}nxt{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}pt{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ me\ nxt\ p\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ pt{\isaliteral{3B}{\isacharsemicolon}}\isanewline
3.799 +val\ {\isaliteral{28}{\isacharparenleft}}p{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}fb{\isaliteral{2C}{\isacharcomma}}nxt{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}pt{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ me\ nxt\ p\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ pt{\isaliteral{3B}{\isacharsemicolon}}\isanewline
3.800 +val\ {\isaliteral{28}{\isacharparenleft}}p{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}fb{\isaliteral{2C}{\isacharcomma}}nxt{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}pt{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ me\ nxt\ p\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ pt{\isaliteral{3B}{\isacharsemicolon}}\isanewline
3.801 +val\ {\isaliteral{28}{\isacharparenleft}}p{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}fb{\isaliteral{2C}{\isacharcomma}}nxt{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}pt{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ me\ nxt\ p\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ pt{\isaliteral{3B}{\isacharsemicolon}}\isanewline
3.802 +val\ {\isaliteral{28}{\isacharparenleft}}p{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}fb{\isaliteral{2C}{\isacharcomma}}nxt{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}pt{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ me\ nxt\ p\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ pt{\isaliteral{3B}{\isacharsemicolon}}\isanewline
3.803 +val\ {\isaliteral{28}{\isacharparenleft}}p{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}fb{\isaliteral{2C}{\isacharcomma}}nxt{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}pt{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ me\ nxt\ p\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ pt{\isaliteral{3B}{\isacharsemicolon}}\isanewline
3.804 +val\ {\isaliteral{28}{\isacharparenleft}}p{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}fb{\isaliteral{2C}{\isacharcomma}}nxt{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}pt{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ me\ nxt\ p\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ pt{\isaliteral{3B}{\isacharsemicolon}}\isanewline
3.805 +val\ {\isaliteral{28}{\isacharparenleft}}p{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}fb{\isaliteral{2C}{\isacharcomma}}nxt{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}pt{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ me\ nxt\ p\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ pt{\isaliteral{3B}{\isacharsemicolon}}\isanewline
3.806 +val\ {\isaliteral{28}{\isacharparenleft}}p{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}fb{\isaliteral{2C}{\isacharcomma}}nxt{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}pt{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ me\ nxt\ p\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ pt{\isaliteral{3B}{\isacharsemicolon}}\isanewline
3.807 +val\ {\isaliteral{28}{\isacharparenleft}}p{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}fb{\isaliteral{2C}{\isacharcomma}}nxt{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}pt{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ me\ nxt\ p\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ pt{\isaliteral{3B}{\isacharsemicolon}}\isanewline
3.808 +val\ {\isaliteral{28}{\isacharparenleft}}p{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}fb{\isaliteral{2C}{\isacharcomma}}nxt{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}pt{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ me\ nxt\ p\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ pt{\isaliteral{3B}{\isacharsemicolon}}\isanewline
3.809 +val\ {\isaliteral{28}{\isacharparenleft}}p{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}fb{\isaliteral{2C}{\isacharcomma}}nxt{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}pt{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ me\ nxt\ p\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ pt{\isaliteral{3B}{\isacharsemicolon}}\isanewline
3.810 +val\ {\isaliteral{28}{\isacharparenleft}}p{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}fb{\isaliteral{2C}{\isacharcomma}}nxt{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}pt{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ me\ nxt\ p\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ pt{\isaliteral{3B}{\isacharsemicolon}}\isanewline
3.811 +val\ {\isaliteral{28}{\isacharparenleft}}p{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}fb{\isaliteral{2C}{\isacharcomma}}nxt{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}pt{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ me\ nxt\ p\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ pt{\isaliteral{3B}{\isacharsemicolon}}\isanewline
3.812 +val\ {\isaliteral{28}{\isacharparenleft}}p{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}fb{\isaliteral{2C}{\isacharcomma}}nxt{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}pt{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ me\ nxt\ p\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ pt{\isaliteral{3B}{\isacharsemicolon}}\isanewline
3.813 +val\ {\isaliteral{28}{\isacharparenleft}}p{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}fb{\isaliteral{2C}{\isacharcomma}}nxt{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}pt{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ me\ nxt\ p\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ pt{\isaliteral{3B}{\isacharsemicolon}}\isanewline
3.814 +val\ {\isaliteral{28}{\isacharparenleft}}p{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}fb{\isaliteral{2C}{\isacharcomma}}nxt{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}pt{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ me\ nxt\ p\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ pt{\isaliteral{3B}{\isacharsemicolon}}\isanewline
3.815 +val\ {\isaliteral{28}{\isacharparenleft}}p{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}fb{\isaliteral{2C}{\isacharcomma}}nxt{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}pt{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ me\ nxt\ p\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ pt{\isaliteral{3B}{\isacharsemicolon}}\isanewline
3.816 +val\ {\isaliteral{28}{\isacharparenleft}}p{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}fb{\isaliteral{2C}{\isacharcomma}}nxt{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}pt{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ me\ nxt\ p\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ pt{\isaliteral{3B}{\isacharsemicolon}}\ \isanewline
3.817 +f{\isadigit{2}}str\ fb{\isaliteral{3B}{\isacharsemicolon}}\isanewline
3.818 +{\isaliteral{2A7D}{\isacharverbatimclose}}\isanewline
3.819 +\isanewline
3.820 +\isacommand{ML}\isamarkupfalse%
3.821 +\ {\isaliteral{7B2A}{\isacharverbatimopen}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{2A}{\isacharasterisk}}check\ koeffizients{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{29}{\isacharparenright}}\isanewline
3.822 +if\ f{\isadigit{2}}str\ fa\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{22}{\isachardoublequote}}{\isaliteral{5B}{\isacharbrackleft}}A\ {\isaliteral{3D}{\isacharequal}}\ {\isadigit{4}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{22}{\isachardoublequote}}\ then\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{29}{\isacharparenright}}\ else\ error\ {\isaliteral{22}{\isachardoublequote}}part{\isaliteral{2E}{\isachardot}}fract{\isaliteral{2E}{\isachardot}}\ eq{\isadigit{4}}{\isaliteral{5F}{\isacharunderscore}}{\isadigit{1}}{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
3.823 +if\ f{\isadigit{2}}str\ fb\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{22}{\isachardoublequote}}{\isaliteral{5B}{\isacharbrackleft}}B\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{2D}{\isacharminus}}{\isadigit{4}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{22}{\isachardoublequote}}\ then\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{29}{\isacharparenright}}\ else\ error\ {\isaliteral{22}{\isachardoublequote}}part{\isaliteral{2E}{\isachardot}}fract{\isaliteral{2E}{\isachardot}}\ eq{\isadigit{4}}{\isaliteral{5F}{\isacharunderscore}}{\isadigit{1}}{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
3.824 +{\isaliteral{2A7D}{\isacharverbatimclose}}%
3.825 +\endisatagML
3.826 +{\isafoldML}%
3.827 +%
3.828 +\isadelimML
3.829 +%
3.830 +\endisadelimML
3.831 +%
3.832 +\isamarkupsubsubsection{substitute expression with solutions%
3.833 +}
3.834 +\isamarkuptrue%
3.835 +%
3.836 +\isadelimML
3.837 +%
3.838 +\endisadelimML
3.839 +%
3.840 +\isatagML
3.841 +\isacommand{ML}\isamarkupfalse%
3.842 +\ {\isaliteral{7B2A}{\isacharverbatimopen}}\isanewline
3.843 +{\isaliteral{2A7D}{\isacharverbatimclose}}\isanewline
3.844 +\isacommand{ML}\isamarkupfalse%
3.845 +\ {\isaliteral{7B2A}{\isacharverbatimopen}}thy{\isaliteral{2A7D}{\isacharverbatimclose}}%
3.846 +\endisatagML
3.847 +{\isafoldML}%
3.848 +%
3.849 +\isadelimML
3.850 +%
3.851 +\endisadelimML
3.852 +%
3.853 +\isamarkupsection{Implement the Specification and the Method%
3.854 +}
3.855 +\isamarkuptrue%
3.856 +%
3.857 +\begin{isamarkuptext}%
3.858 +==============================================%
3.859 +\end{isamarkuptext}%
3.860 +\isamarkuptrue%
3.861 +%
3.862 +\isamarkupsubsection{Define the Field Descriptions for the specification%
3.863 +}
3.864 +\isamarkuptrue%
3.865 +\isacommand{consts}\isamarkupfalse%
3.866 +\isanewline
3.867 +\ \ filterExpression\ \ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}bool\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{3E}{\isachargreater}}\ una{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
3.868 +\ \ stepResponse\ \ \ \ \ \ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}bool\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{3E}{\isachargreater}}\ una{\isaliteral{22}{\isachardoublequoteclose}}%
3.869 +\isamarkupsubsection{Define the Specification%
3.870 +}
3.871 +\isamarkuptrue%
3.872 +%
3.873 +\isadelimML
3.874 +%
3.875 +\endisadelimML
3.876 +%
3.877 +\isatagML
3.878 +\isacommand{ML}\isamarkupfalse%
3.879 +\ {\isaliteral{7B2A}{\isacharverbatimopen}}\isanewline
3.880 +store{\isaliteral{5F}{\isacharunderscore}}pbt\isanewline
3.881 +\ {\isaliteral{28}{\isacharparenleft}}prep{\isaliteral{5F}{\isacharunderscore}}pbt\ thy\ {\isaliteral{22}{\isachardoublequote}}pbl{\isaliteral{5F}{\isacharunderscore}}SP{\isaliteral{22}{\isachardoublequote}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ e{\isaliteral{5F}{\isacharunderscore}}pblID\isanewline
3.882 +\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{22}{\isachardoublequote}}SignalProcessing{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{2C}{\isacharcomma}}\ e{\isaliteral{5F}{\isacharunderscore}}rls{\isaliteral{2C}{\isacharcomma}}\ NONE{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
3.883 +store{\isaliteral{5F}{\isacharunderscore}}pbt\isanewline
3.884 +\ {\isaliteral{28}{\isacharparenleft}}prep{\isaliteral{5F}{\isacharunderscore}}pbt\ thy\ {\isaliteral{22}{\isachardoublequote}}pbl{\isaliteral{5F}{\isacharunderscore}}SP{\isaliteral{5F}{\isacharunderscore}}Ztrans{\isaliteral{22}{\isachardoublequote}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ e{\isaliteral{5F}{\isacharunderscore}}pblID\isanewline
3.885 +\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{22}{\isachardoublequote}}Z{\isaliteral{5F}{\isacharunderscore}}Transform{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}{\isaliteral{22}{\isachardoublequote}}SignalProcessing{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{2C}{\isacharcomma}}\ e{\isaliteral{5F}{\isacharunderscore}}rls{\isaliteral{2C}{\isacharcomma}}\ NONE{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
3.886 +{\isaliteral{2A7D}{\isacharverbatimclose}}\isanewline
3.887 +\isacommand{ML}\isamarkupfalse%
3.888 +\ {\isaliteral{7B2A}{\isacharverbatimopen}}thy{\isaliteral{2A7D}{\isacharverbatimclose}}\isanewline
3.889 +\isacommand{ML}\isamarkupfalse%
3.890 +\ {\isaliteral{7B2A}{\isacharverbatimopen}}\isanewline
3.891 +store{\isaliteral{5F}{\isacharunderscore}}pbt\isanewline
3.892 +\ {\isaliteral{28}{\isacharparenleft}}prep{\isaliteral{5F}{\isacharunderscore}}pbt\ thy\ {\isaliteral{22}{\isachardoublequote}}pbl{\isaliteral{5F}{\isacharunderscore}}SP{\isaliteral{5F}{\isacharunderscore}}Ztrans{\isaliteral{5F}{\isacharunderscore}}inv{\isaliteral{22}{\isachardoublequote}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ e{\isaliteral{5F}{\isacharunderscore}}pblID\isanewline
3.893 +\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{22}{\isachardoublequote}}inverse{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{22}{\isachardoublequote}}Z{\isaliteral{5F}{\isacharunderscore}}Transform{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{22}{\isachardoublequote}}SignalProcessing{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{2C}{\isacharcomma}}\isanewline
3.894 +\ \ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{22}{\isachardoublequote}}{\isaliteral{23}{\isacharhash}}Given{\isaliteral{22}{\isachardoublequote}}\ {\isaliteral{2C}{\isacharcomma}}{\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{22}{\isachardoublequote}}filterExpression\ X{\isaliteral{5F}{\isacharunderscore}}eq{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{2C}{\isacharcomma}}\isanewline
3.895 +\ \ \ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{22}{\isachardoublequote}}{\isaliteral{23}{\isacharhash}}Find{\isaliteral{22}{\isachardoublequote}}\ \ {\isaliteral{2C}{\isacharcomma}}{\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{22}{\isachardoublequote}}stepResponse\ n{\isaliteral{5F}{\isacharunderscore}}eq{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{29}{\isacharparenright}}\isanewline
3.896 +\ \ {\isaliteral{5D}{\isacharbrackright}}{\isaliteral{2C}{\isacharcomma}}\isanewline
3.897 +\ \ append{\isaliteral{5F}{\isacharunderscore}}rls\ {\isaliteral{22}{\isachardoublequote}}e{\isaliteral{5F}{\isacharunderscore}}rls{\isaliteral{22}{\isachardoublequote}}\ e{\isaliteral{5F}{\isacharunderscore}}rls\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{2A}{\isacharasterisk}}for\ preds\ in\ where{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{2C}{\isacharcomma}}\ NONE{\isaliteral{2C}{\isacharcomma}}\ \isanewline
3.898 +\ \ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{22}{\isachardoublequote}}SignalProcessing{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}{\isaliteral{22}{\isachardoublequote}}Z{\isaliteral{5F}{\isacharunderscore}}Transform{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}{\isaliteral{22}{\isachardoublequote}}inverse{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
3.899 +\isanewline
3.900 +show{\isaliteral{5F}{\isacharunderscore}}ptyps{\isaliteral{28}{\isacharparenleft}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
3.901 +get{\isaliteral{5F}{\isacharunderscore}}pbt\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{22}{\isachardoublequote}}inverse{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}{\isaliteral{22}{\isachardoublequote}}Z{\isaliteral{5F}{\isacharunderscore}}Transform{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}{\isaliteral{22}{\isachardoublequote}}SignalProcessing{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
3.902 +{\isaliteral{2A7D}{\isacharverbatimclose}}%
3.903 +\endisatagML
3.904 +{\isafoldML}%
3.905 +%
3.906 +\isadelimML
3.907 +%
3.908 +\endisadelimML
3.909 +%
3.910 +\isamarkupsubsection{Define Name and Signature for the Method%
3.911 +}
3.912 +\isamarkuptrue%
3.913 +\isacommand{consts}\isamarkupfalse%
3.914 +\isanewline
3.915 +\ \ InverseZTransform\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5B}{\isacharbrackleft}}bool{\isaliteral{2C}{\isacharcomma}}\ bool{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{3E}{\isachargreater}}\ bool{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
3.916 +\ \ \ \ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{28}{\isacharparenleft}}Script\ InverseZTransform\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5F}{\isacharunderscore}}\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{2F}{\isacharslash}}{\isaliteral{2F}{\isacharslash}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\ {\isadigit{9}}{\isaliteral{29}{\isacharparenright}}%
3.917 +\isamarkupsubsection{Setup Parent Nodes in Hierarchy of Method%
3.918 +}
3.919 +\isamarkuptrue%
3.920 +%
3.921 +\isadelimML
3.922 +%
3.923 +\endisadelimML
3.924 +%
3.925 +\isatagML
3.926 +\isacommand{ML}\isamarkupfalse%
3.927 +\ {\isaliteral{7B2A}{\isacharverbatimopen}}\isanewline
3.928 +store{\isaliteral{5F}{\isacharunderscore}}met\isanewline
3.929 +\ {\isaliteral{28}{\isacharparenleft}}prep{\isaliteral{5F}{\isacharunderscore}}met\ thy\ {\isaliteral{22}{\isachardoublequote}}met{\isaliteral{5F}{\isacharunderscore}}SP{\isaliteral{22}{\isachardoublequote}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ e{\isaliteral{5F}{\isacharunderscore}}metID\isanewline
3.930 +\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{22}{\isachardoublequote}}SignalProcessing{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{2C}{\isacharcomma}}\isanewline
3.931 +\ \ \ {\isaliteral{7B}{\isacharbraceleft}}rew{\isaliteral{5F}{\isacharunderscore}}ord{\isaliteral{27}{\isacharprime}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{22}{\isachardoublequote}}tless{\isaliteral{5F}{\isacharunderscore}}true{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\ rls{\isaliteral{27}{\isacharprime}}{\isaliteral{3D}{\isacharequal}}\ e{\isaliteral{5F}{\isacharunderscore}}rls{\isaliteral{2C}{\isacharcomma}}\ calc\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{2C}{\isacharcomma}}\ srls\ {\isaliteral{3D}{\isacharequal}}\ e{\isaliteral{5F}{\isacharunderscore}}rls{\isaliteral{2C}{\isacharcomma}}\ prls\ {\isaliteral{3D}{\isacharequal}}\ e{\isaliteral{5F}{\isacharunderscore}}rls{\isaliteral{2C}{\isacharcomma}}\isanewline
3.932 +\ \ \ \ crls\ {\isaliteral{3D}{\isacharequal}}\ e{\isaliteral{5F}{\isacharunderscore}}rls{\isaliteral{2C}{\isacharcomma}}\ nrls\ {\isaliteral{3D}{\isacharequal}}\ e{\isaliteral{5F}{\isacharunderscore}}rls{\isaliteral{7D}{\isacharbraceright}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{22}{\isachardoublequote}}empty{\isaliteral{5F}{\isacharunderscore}}script{\isaliteral{22}{\isachardoublequote}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
3.933 +store{\isaliteral{5F}{\isacharunderscore}}met\isanewline
3.934 +\ {\isaliteral{28}{\isacharparenleft}}prep{\isaliteral{5F}{\isacharunderscore}}met\ thy\ {\isaliteral{22}{\isachardoublequote}}met{\isaliteral{5F}{\isacharunderscore}}SP{\isaliteral{5F}{\isacharunderscore}}Ztrans{\isaliteral{22}{\isachardoublequote}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ e{\isaliteral{5F}{\isacharunderscore}}metID\isanewline
3.935 +\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{22}{\isachardoublequote}}SignalProcessing{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{22}{\isachardoublequote}}Z{\isaliteral{5F}{\isacharunderscore}}Transform{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{2C}{\isacharcomma}}\isanewline
3.936 +\ \ \ {\isaliteral{7B}{\isacharbraceleft}}rew{\isaliteral{5F}{\isacharunderscore}}ord{\isaliteral{27}{\isacharprime}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{22}{\isachardoublequote}}tless{\isaliteral{5F}{\isacharunderscore}}true{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\ rls{\isaliteral{27}{\isacharprime}}{\isaliteral{3D}{\isacharequal}}\ e{\isaliteral{5F}{\isacharunderscore}}rls{\isaliteral{2C}{\isacharcomma}}\ calc\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{2C}{\isacharcomma}}\ srls\ {\isaliteral{3D}{\isacharequal}}\ e{\isaliteral{5F}{\isacharunderscore}}rls{\isaliteral{2C}{\isacharcomma}}\ prls\ {\isaliteral{3D}{\isacharequal}}\ e{\isaliteral{5F}{\isacharunderscore}}rls{\isaliteral{2C}{\isacharcomma}}\isanewline
3.937 +\ \ \ \ crls\ {\isaliteral{3D}{\isacharequal}}\ e{\isaliteral{5F}{\isacharunderscore}}rls{\isaliteral{2C}{\isacharcomma}}\ nrls\ {\isaliteral{3D}{\isacharequal}}\ e{\isaliteral{5F}{\isacharunderscore}}rls{\isaliteral{7D}{\isacharbraceright}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{22}{\isachardoublequote}}empty{\isaliteral{5F}{\isacharunderscore}}script{\isaliteral{22}{\isachardoublequote}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
3.938 +{\isaliteral{2A7D}{\isacharverbatimclose}}\isanewline
3.939 +\isacommand{ML}\isamarkupfalse%
3.940 +\ {\isaliteral{7B2A}{\isacharverbatimopen}}\isanewline
3.941 +store{\isaliteral{5F}{\isacharunderscore}}met\isanewline
3.942 +\ {\isaliteral{28}{\isacharparenleft}}prep{\isaliteral{5F}{\isacharunderscore}}met\ thy\ {\isaliteral{22}{\isachardoublequote}}met{\isaliteral{5F}{\isacharunderscore}}SP{\isaliteral{5F}{\isacharunderscore}}Ztrans{\isaliteral{5F}{\isacharunderscore}}inv{\isaliteral{22}{\isachardoublequote}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ e{\isaliteral{5F}{\isacharunderscore}}metID\isanewline
3.943 +\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{22}{\isachardoublequote}}SignalProcessing{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{22}{\isachardoublequote}}Z{\isaliteral{5F}{\isacharunderscore}}Transform{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{22}{\isachardoublequote}}inverse{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{2C}{\isacharcomma}}\ \isanewline
3.944 +\ \ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{22}{\isachardoublequote}}{\isaliteral{23}{\isacharhash}}Given{\isaliteral{22}{\isachardoublequote}}\ {\isaliteral{2C}{\isacharcomma}}{\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{22}{\isachardoublequote}}filterExpression\ X{\isaliteral{5F}{\isacharunderscore}}eq{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{2C}{\isacharcomma}}\isanewline
3.945 +\ \ \ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{22}{\isachardoublequote}}{\isaliteral{23}{\isacharhash}}Find{\isaliteral{22}{\isachardoublequote}}\ \ {\isaliteral{2C}{\isacharcomma}}{\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{22}{\isachardoublequote}}stepResponse\ n{\isaliteral{5F}{\isacharunderscore}}eq{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{29}{\isacharparenright}}\isanewline
3.946 +\ \ {\isaliteral{5D}{\isacharbrackright}}{\isaliteral{2C}{\isacharcomma}}\isanewline
3.947 +\ \ \ {\isaliteral{7B}{\isacharbraceleft}}rew{\isaliteral{5F}{\isacharunderscore}}ord{\isaliteral{27}{\isacharprime}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{22}{\isachardoublequote}}tless{\isaliteral{5F}{\isacharunderscore}}true{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\ rls{\isaliteral{27}{\isacharprime}}{\isaliteral{3D}{\isacharequal}}\ e{\isaliteral{5F}{\isacharunderscore}}rls{\isaliteral{2C}{\isacharcomma}}\ calc\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{2C}{\isacharcomma}}\ srls\ {\isaliteral{3D}{\isacharequal}}\ e{\isaliteral{5F}{\isacharunderscore}}rls{\isaliteral{2C}{\isacharcomma}}\ prls\ {\isaliteral{3D}{\isacharequal}}\ e{\isaliteral{5F}{\isacharunderscore}}rls{\isaliteral{2C}{\isacharcomma}}\isanewline
3.948 +\ \ \ \ crls\ {\isaliteral{3D}{\isacharequal}}\ e{\isaliteral{5F}{\isacharunderscore}}rls{\isaliteral{2C}{\isacharcomma}}\ nrls\ {\isaliteral{3D}{\isacharequal}}\ e{\isaliteral{5F}{\isacharunderscore}}rls{\isaliteral{7D}{\isacharbraceright}}{\isaliteral{2C}{\isacharcomma}}\isanewline
3.949 +\ \ {\isaliteral{22}{\isachardoublequote}}empty{\isaliteral{5F}{\isacharunderscore}}script{\isaliteral{22}{\isachardoublequote}}\isanewline
3.950 +\ {\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
3.951 +{\isaliteral{2A7D}{\isacharverbatimclose}}\isanewline
3.952 +\isacommand{ML}\isamarkupfalse%
3.953 +\ {\isaliteral{7B2A}{\isacharverbatimopen}}\isanewline
3.954 +store{\isaliteral{5F}{\isacharunderscore}}met\isanewline
3.955 +\ {\isaliteral{28}{\isacharparenleft}}prep{\isaliteral{5F}{\isacharunderscore}}met\ thy\ {\isaliteral{22}{\isachardoublequote}}met{\isaliteral{5F}{\isacharunderscore}}SP{\isaliteral{5F}{\isacharunderscore}}Ztrans{\isaliteral{5F}{\isacharunderscore}}inv{\isaliteral{22}{\isachardoublequote}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ e{\isaliteral{5F}{\isacharunderscore}}metID\isanewline
3.956 +\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{22}{\isachardoublequote}}SignalProcessing{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{22}{\isachardoublequote}}Z{\isaliteral{5F}{\isacharunderscore}}Transform{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{22}{\isachardoublequote}}inverse{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{2C}{\isacharcomma}}\ \isanewline
3.957 +\ \ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{22}{\isachardoublequote}}{\isaliteral{23}{\isacharhash}}Given{\isaliteral{22}{\isachardoublequote}}\ {\isaliteral{2C}{\isacharcomma}}{\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{22}{\isachardoublequote}}filterExpression\ X{\isaliteral{5F}{\isacharunderscore}}eq{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{2C}{\isacharcomma}}\isanewline
3.958 +\ \ \ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{22}{\isachardoublequote}}{\isaliteral{23}{\isacharhash}}Find{\isaliteral{22}{\isachardoublequote}}\ \ {\isaliteral{2C}{\isacharcomma}}{\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{22}{\isachardoublequote}}stepResponse\ n{\isaliteral{5F}{\isacharunderscore}}eq{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{29}{\isacharparenright}}\isanewline
3.959 +\ \ {\isaliteral{5D}{\isacharbrackright}}{\isaliteral{2C}{\isacharcomma}}\isanewline
3.960 +\ \ \ {\isaliteral{7B}{\isacharbraceleft}}rew{\isaliteral{5F}{\isacharunderscore}}ord{\isaliteral{27}{\isacharprime}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{22}{\isachardoublequote}}tless{\isaliteral{5F}{\isacharunderscore}}true{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\ rls{\isaliteral{27}{\isacharprime}}{\isaliteral{3D}{\isacharequal}}\ e{\isaliteral{5F}{\isacharunderscore}}rls{\isaliteral{2C}{\isacharcomma}}\ calc\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{2C}{\isacharcomma}}\ srls\ {\isaliteral{3D}{\isacharequal}}\ e{\isaliteral{5F}{\isacharunderscore}}rls{\isaliteral{2C}{\isacharcomma}}\ prls\ {\isaliteral{3D}{\isacharequal}}\ e{\isaliteral{5F}{\isacharunderscore}}rls{\isaliteral{2C}{\isacharcomma}}\isanewline
3.961 +\ \ \ \ crls\ {\isaliteral{3D}{\isacharequal}}\ e{\isaliteral{5F}{\isacharunderscore}}rls{\isaliteral{2C}{\isacharcomma}}\ nrls\ {\isaliteral{3D}{\isacharequal}}\ e{\isaliteral{5F}{\isacharunderscore}}rls{\isaliteral{7D}{\isacharbraceright}}{\isaliteral{2C}{\isacharcomma}}\isanewline
3.962 +\ \ {\isaliteral{22}{\isachardoublequote}}Script\ InverseZTransform\ {\isaliteral{28}{\isacharparenleft}}Xeq{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}bool{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{22}{\isachardoublequote}}\ {\isaliteral{5E}{\isacharcircum}}\isanewline
3.963 +\ \ {\isaliteral{22}{\isachardoublequote}}\ {\isaliteral{28}{\isacharparenleft}}let\ X\ {\isaliteral{3D}{\isacharequal}}\ Take\ Xeq{\isaliteral{3B}{\isacharsemicolon}}{\isaliteral{22}{\isachardoublequote}}\ {\isaliteral{5E}{\isacharcircum}}\isanewline
3.964 +\ \ {\isaliteral{22}{\isachardoublequote}}\ \ \ \ \ \ X\ {\isaliteral{3D}{\isacharequal}}\ Rewrite\ ruleZY\ False\ X{\isaliteral{22}{\isachardoublequote}}\ {\isaliteral{5E}{\isacharcircum}}\isanewline
3.965 +\ \ {\isaliteral{22}{\isachardoublequote}}\ \ in\ X{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}\isanewline
3.966 +\ {\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
3.967 +\isanewline
3.968 +show{\isaliteral{5F}{\isacharunderscore}}mets{\isaliteral{28}{\isacharparenleft}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
3.969 +get{\isaliteral{5F}{\isacharunderscore}}met\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{22}{\isachardoublequote}}SignalProcessing{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}{\isaliteral{22}{\isachardoublequote}}Z{\isaliteral{5F}{\isacharunderscore}}Transform{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}{\isaliteral{22}{\isachardoublequote}}inverse{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
3.970 +{\isaliteral{2A7D}{\isacharverbatimclose}}%
3.971 +\endisatagML
3.972 +{\isafoldML}%
3.973 +%
3.974 +\isadelimML
3.975 +%
3.976 +\endisadelimML
3.977 +%
3.978 +\isamarkupsection{Program in CTP-based language%
3.979 +}
3.980 +\isamarkuptrue%
3.981 +%
3.982 +\begin{isamarkuptext}%
3.983 +=================================%
3.984 +\end{isamarkuptext}%
3.985 +\isamarkuptrue%
3.986 +%
3.987 +\isamarkupsubsection{Stepwise extend Program%
3.988 +}
3.989 +\isamarkuptrue%
3.990 +%
3.991 +\isadelimML
3.992 +%
3.993 +\endisadelimML
3.994 +%
3.995 +\isatagML
3.996 +\isacommand{ML}\isamarkupfalse%
3.997 +\ {\isaliteral{7B2A}{\isacharverbatimopen}}\isanewline
3.998 +val\ str\ {\isaliteral{3D}{\isacharequal}}\ \isanewline
3.999 +{\isaliteral{22}{\isachardoublequote}}Script\ InverseZTransform\ {\isaliteral{28}{\isacharparenleft}}Xeq{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}bool{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{22}{\isachardoublequote}}\ {\isaliteral{5E}{\isacharcircum}}\isanewline
3.1000 +{\isaliteral{22}{\isachardoublequote}}\ Xeq{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
3.1001 +{\isaliteral{2A7D}{\isacharverbatimclose}}\isanewline
3.1002 +\isacommand{ML}\isamarkupfalse%
3.1003 +\ {\isaliteral{7B2A}{\isacharverbatimopen}}\isanewline
3.1004 +val\ str\ {\isaliteral{3D}{\isacharequal}}\ \isanewline
3.1005 +{\isaliteral{22}{\isachardoublequote}}Script\ InverseZTransform\ {\isaliteral{28}{\isacharparenleft}}Xeq{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}bool{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{22}{\isachardoublequote}}\ {\isaliteral{5E}{\isacharcircum}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{28}{\isacharparenleft}}{\isadigit{1}}{\isaliteral{2F}{\isacharslash}}z{\isaliteral{29}{\isacharparenright}}\ instead\ of\ z\ {\isaliteral{5E}{\isacharcircum}}{\isaliteral{5E}{\isacharcircum}}{\isaliteral{5E}{\isacharcircum}}\ {\isaliteral{2D}{\isacharminus}}{\isadigit{1}}{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{29}{\isacharparenright}}\isanewline
3.1006 +{\isaliteral{22}{\isachardoublequote}}\ {\isaliteral{28}{\isacharparenleft}}let\ X\ {\isaliteral{3D}{\isacharequal}}\ Take\ Xeq{\isaliteral{3B}{\isacharsemicolon}}{\isaliteral{22}{\isachardoublequote}}\ {\isaliteral{5E}{\isacharcircum}}\isanewline
3.1007 +{\isaliteral{22}{\isachardoublequote}}\ \ \ \ \ \ X{\isaliteral{27}{\isacharprime}}\ {\isaliteral{3D}{\isacharequal}}\ Rewrite\ ruleZY\ False\ X{\isaliteral{3B}{\isacharsemicolon}}{\isaliteral{22}{\isachardoublequote}}\ {\isaliteral{5E}{\isacharcircum}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{2A}{\isacharasterisk}}z\ {\isaliteral{2A}{\isacharasterisk}}\ denominator{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{29}{\isacharparenright}}\isanewline
3.1008 +{\isaliteral{22}{\isachardoublequote}}\ \ \ \ \ \ X{\isaliteral{27}{\isacharprime}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}Rewrite{\isaliteral{5F}{\isacharunderscore}}Set\ norm{\isaliteral{5F}{\isacharunderscore}}Rational\ False{\isaliteral{29}{\isacharparenright}}\ X{\isaliteral{27}{\isacharprime}}{\isaliteral{22}{\isachardoublequote}}\ {\isaliteral{5E}{\isacharcircum}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{2A}{\isacharasterisk}}simplify{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{29}{\isacharparenright}}\isanewline
3.1009 +{\isaliteral{22}{\isachardoublequote}}\ \ in\ X{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
3.1010 +{\isaliteral{28}{\isacharparenleft}}{\isaliteral{2A}{\isacharasterisk}}NONE{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{29}{\isacharparenright}}\isanewline
3.1011 +{\isaliteral{22}{\isachardoublequote}}Script\ InverseZTransform\ {\isaliteral{28}{\isacharparenleft}}Xeq{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}bool{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{22}{\isachardoublequote}}\ {\isaliteral{5E}{\isacharcircum}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{28}{\isacharparenleft}}{\isadigit{1}}{\isaliteral{2F}{\isacharslash}}z{\isaliteral{29}{\isacharparenright}}\ instead\ of\ z\ {\isaliteral{5E}{\isacharcircum}}{\isaliteral{5E}{\isacharcircum}}{\isaliteral{5E}{\isacharcircum}}\ {\isaliteral{2D}{\isacharminus}}{\isadigit{1}}{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{29}{\isacharparenright}}\isanewline
3.1012 +{\isaliteral{22}{\isachardoublequote}}\ {\isaliteral{28}{\isacharparenleft}}let\ X\ {\isaliteral{3D}{\isacharequal}}\ Take\ Xeq{\isaliteral{3B}{\isacharsemicolon}}{\isaliteral{22}{\isachardoublequote}}\ {\isaliteral{5E}{\isacharcircum}}\isanewline
3.1013 +{\isaliteral{22}{\isachardoublequote}}\ \ \ \ \ \ X{\isaliteral{27}{\isacharprime}}\ {\isaliteral{3D}{\isacharequal}}\ Rewrite\ ruleZY\ False\ X{\isaliteral{3B}{\isacharsemicolon}}{\isaliteral{22}{\isachardoublequote}}\ {\isaliteral{5E}{\isacharcircum}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{2A}{\isacharasterisk}}z\ {\isaliteral{2A}{\isacharasterisk}}\ denominator{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{29}{\isacharparenright}}\isanewline
3.1014 +{\isaliteral{22}{\isachardoublequote}}\ \ \ \ \ \ X{\isaliteral{27}{\isacharprime}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}Rewrite{\isaliteral{5F}{\isacharunderscore}}Set\ norm{\isaliteral{5F}{\isacharunderscore}}Rational\ False{\isaliteral{29}{\isacharparenright}}\ X{\isaliteral{27}{\isacharprime}}{\isaliteral{3B}{\isacharsemicolon}}{\isaliteral{22}{\isachardoublequote}}\ {\isaliteral{5E}{\isacharcircum}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{2A}{\isacharasterisk}}simplify{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{29}{\isacharparenright}}\isanewline
3.1015 +{\isaliteral{22}{\isachardoublequote}}\ \ \ \ \ \ X{\isaliteral{27}{\isacharprime}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}SubProblem\ {\isaliteral{28}{\isacharparenleft}}Isac{\isaliteral{27}{\isacharprime}}{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5B}{\isacharbrackleft}}pqFormula{\isaliteral{2C}{\isacharcomma}}degree{\isaliteral{5F}{\isacharunderscore}}{\isadigit{2}}{\isaliteral{2C}{\isacharcomma}}polynomial{\isaliteral{2C}{\isacharcomma}}univariate{\isaliteral{2C}{\isacharcomma}}equation{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5B}{\isacharbrackleft}}no{\isaliteral{5F}{\isacharunderscore}}met{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{29}{\isacharparenright}}\ \ \ {\isaliteral{22}{\isachardoublequote}}\ {\isaliteral{5E}{\isacharcircum}}\isanewline
3.1016 +\ \ \ \ {\isaliteral{22}{\isachardoublequote}}\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isaliteral{5B}{\isacharbrackleft}}BOOL\ e{\isaliteral{5F}{\isacharunderscore}}e{\isaliteral{2C}{\isacharcomma}}\ REAL\ v{\isaliteral{5F}{\isacharunderscore}}v{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}\ {\isaliteral{5E}{\isacharcircum}}\isanewline
3.1017 +{\isaliteral{22}{\isachardoublequote}}\ \ in\ X{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
3.1018 +{\isaliteral{2A7D}{\isacharverbatimclose}}\isanewline
3.1019 +\isacommand{ML}\isamarkupfalse%
3.1020 +\ {\isaliteral{7B2A}{\isacharverbatimopen}}\isanewline
3.1021 +val\ str\ {\isaliteral{3D}{\isacharequal}}\ \isanewline
3.1022 +{\isaliteral{22}{\isachardoublequote}}Script\ InverseZTransform\ {\isaliteral{28}{\isacharparenleft}}Xeq{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}bool{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{22}{\isachardoublequote}}\ {\isaliteral{5E}{\isacharcircum}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{28}{\isacharparenleft}}{\isadigit{1}}{\isaliteral{2F}{\isacharslash}}z{\isaliteral{29}{\isacharparenright}}\ instead\ of\ z\ {\isaliteral{5E}{\isacharcircum}}{\isaliteral{5E}{\isacharcircum}}{\isaliteral{5E}{\isacharcircum}}\ {\isaliteral{2D}{\isacharminus}}{\isadigit{1}}{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{29}{\isacharparenright}}\isanewline
3.1023 +{\isaliteral{22}{\isachardoublequote}}\ {\isaliteral{28}{\isacharparenleft}}let\ X\ {\isaliteral{3D}{\isacharequal}}\ Take\ Xeq{\isaliteral{3B}{\isacharsemicolon}}{\isaliteral{22}{\isachardoublequote}}\ {\isaliteral{5E}{\isacharcircum}}\isanewline
3.1024 +{\isaliteral{22}{\isachardoublequote}}\ \ \ \ \ \ X{\isaliteral{27}{\isacharprime}}\ {\isaliteral{3D}{\isacharequal}}\ Rewrite\ ruleZY\ False\ X{\isaliteral{3B}{\isacharsemicolon}}{\isaliteral{22}{\isachardoublequote}}\ {\isaliteral{5E}{\isacharcircum}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{2A}{\isacharasterisk}}z\ {\isaliteral{2A}{\isacharasterisk}}\ denominator{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{29}{\isacharparenright}}\isanewline
3.1025 +{\isaliteral{22}{\isachardoublequote}}\ \ \ \ \ \ X{\isaliteral{27}{\isacharprime}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}Rewrite{\isaliteral{5F}{\isacharunderscore}}Set\ norm{\isaliteral{5F}{\isacharunderscore}}Rational\ False{\isaliteral{29}{\isacharparenright}}\ X{\isaliteral{27}{\isacharprime}}{\isaliteral{3B}{\isacharsemicolon}}{\isaliteral{22}{\isachardoublequote}}\ {\isaliteral{5E}{\isacharcircum}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{2A}{\isacharasterisk}}simplify{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{29}{\isacharparenright}}\isanewline
3.1026 +{\isaliteral{22}{\isachardoublequote}}\ \ \ \ \ \ funterm\ {\isaliteral{3D}{\isacharequal}}\ rhs\ X{\isaliteral{27}{\isacharprime}}{\isaliteral{22}{\isachardoublequote}}\ {\isaliteral{5E}{\isacharcircum}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{2A}{\isacharasterisk}}drop\ X{\isaliteral{27}{\isacharprime}}{\isaliteral{3D}{\isacharequal}}\ for\ equation\ solving{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{29}{\isacharparenright}}\isanewline
3.1027 +{\isaliteral{22}{\isachardoublequote}}\ \ in\ X{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
3.1028 +{\isaliteral{2A7D}{\isacharverbatimclose}}\isanewline
3.1029 +\isacommand{ML}\isamarkupfalse%
3.1030 +\ {\isaliteral{7B2A}{\isacharverbatimopen}}\isanewline
3.1031 +parse\ thy\ str{\isaliteral{3B}{\isacharsemicolon}}\isanewline
3.1032 +val\ sc\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{28}{\isacharparenleft}}inst{\isaliteral{5F}{\isacharunderscore}}abs\ thy{\isaliteral{29}{\isacharparenright}}\ o\ term{\isaliteral{5F}{\isacharunderscore}}of\ o\ the\ o\ {\isaliteral{28}{\isacharparenleft}}parse\ thy{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}\ str{\isaliteral{3B}{\isacharsemicolon}}\isanewline
3.1033 +atomty\ sc{\isaliteral{3B}{\isacharsemicolon}}\isanewline
3.1034 +\isanewline
3.1035 +{\isaliteral{2A7D}{\isacharverbatimclose}}\isanewline
3.1036 +\isacommand{ML}\isamarkupfalse%
3.1037 +\ {\isaliteral{7B2A}{\isacharverbatimopen}}\isanewline
3.1038 +term{\isadigit{2}}str\ sc{\isaliteral{3B}{\isacharsemicolon}}\isanewline
3.1039 +atomty\ sc\isanewline
3.1040 +{\isaliteral{2A7D}{\isacharverbatimclose}}%
3.1041 +\endisatagML
3.1042 +{\isafoldML}%
3.1043 +%
3.1044 +\isadelimML
3.1045 +%
3.1046 +\endisadelimML
3.1047 +%
3.1048 +\isamarkupsubsection{Store Final Version of Program for Execution%
3.1049 +}
3.1050 +\isamarkuptrue%
3.1051 +%
3.1052 +\isadelimML
3.1053 +%
3.1054 +\endisadelimML
3.1055 +%
3.1056 +\isatagML
3.1057 +\isacommand{ML}\isamarkupfalse%
3.1058 +\ {\isaliteral{7B2A}{\isacharverbatimopen}}\isanewline
3.1059 +store{\isaliteral{5F}{\isacharunderscore}}met\isanewline
3.1060 +\ {\isaliteral{28}{\isacharparenleft}}prep{\isaliteral{5F}{\isacharunderscore}}met\ thy\ {\isaliteral{22}{\isachardoublequote}}met{\isaliteral{5F}{\isacharunderscore}}SP{\isaliteral{5F}{\isacharunderscore}}Ztrans{\isaliteral{5F}{\isacharunderscore}}inv{\isaliteral{22}{\isachardoublequote}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ e{\isaliteral{5F}{\isacharunderscore}}metID\isanewline
3.1061 +\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{22}{\isachardoublequote}}SignalProcessing{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{22}{\isachardoublequote}}Z{\isaliteral{5F}{\isacharunderscore}}Transform{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{22}{\isachardoublequote}}inverse{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{2C}{\isacharcomma}}\ \isanewline
3.1062 +\ \ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{22}{\isachardoublequote}}{\isaliteral{23}{\isacharhash}}Given{\isaliteral{22}{\isachardoublequote}}\ {\isaliteral{2C}{\isacharcomma}}{\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{22}{\isachardoublequote}}filterExpression\ X{\isaliteral{5F}{\isacharunderscore}}eq{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{2C}{\isacharcomma}}\isanewline
3.1063 +\ \ \ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{22}{\isachardoublequote}}{\isaliteral{23}{\isacharhash}}Find{\isaliteral{22}{\isachardoublequote}}\ \ {\isaliteral{2C}{\isacharcomma}}{\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{22}{\isachardoublequote}}stepResponse\ n{\isaliteral{5F}{\isacharunderscore}}eq{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{29}{\isacharparenright}}\isanewline
3.1064 +\ \ {\isaliteral{5D}{\isacharbrackright}}{\isaliteral{2C}{\isacharcomma}}\isanewline
3.1065 +\ \ \ {\isaliteral{7B}{\isacharbraceleft}}rew{\isaliteral{5F}{\isacharunderscore}}ord{\isaliteral{27}{\isacharprime}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{22}{\isachardoublequote}}tless{\isaliteral{5F}{\isacharunderscore}}true{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\ rls{\isaliteral{27}{\isacharprime}}{\isaliteral{3D}{\isacharequal}}\ e{\isaliteral{5F}{\isacharunderscore}}rls{\isaliteral{2C}{\isacharcomma}}\ calc\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{2C}{\isacharcomma}}\ srls\ {\isaliteral{3D}{\isacharequal}}\ e{\isaliteral{5F}{\isacharunderscore}}rls{\isaliteral{2C}{\isacharcomma}}\ prls\ {\isaliteral{3D}{\isacharequal}}\ e{\isaliteral{5F}{\isacharunderscore}}rls{\isaliteral{2C}{\isacharcomma}}\isanewline
3.1066 +\ \ \ \ crls\ {\isaliteral{3D}{\isacharequal}}\ e{\isaliteral{5F}{\isacharunderscore}}rls{\isaliteral{2C}{\isacharcomma}}\ nrls\ {\isaliteral{3D}{\isacharequal}}\ e{\isaliteral{5F}{\isacharunderscore}}rls{\isaliteral{7D}{\isacharbraceright}}{\isaliteral{2C}{\isacharcomma}}\isanewline
3.1067 +{\isaliteral{22}{\isachardoublequote}}Script\ InverseZTransform\ {\isaliteral{28}{\isacharparenleft}}X{\isaliteral{5F}{\isacharunderscore}}eq{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}bool{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{22}{\isachardoublequote}}\ {\isaliteral{5E}{\isacharcircum}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{28}{\isacharparenleft}}{\isadigit{1}}{\isaliteral{2F}{\isacharslash}}z{\isaliteral{29}{\isacharparenright}}\ instead\ of\ z\ {\isaliteral{5E}{\isacharcircum}}{\isaliteral{5E}{\isacharcircum}}{\isaliteral{5E}{\isacharcircum}}\ {\isaliteral{2D}{\isacharminus}}{\isadigit{1}}{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{29}{\isacharparenright}}\isanewline
3.1068 +{\isaliteral{22}{\isachardoublequote}}\ {\isaliteral{28}{\isacharparenleft}}let\ X\ {\isaliteral{3D}{\isacharequal}}\ Take\ X{\isaliteral{5F}{\isacharunderscore}}eq{\isaliteral{3B}{\isacharsemicolon}}{\isaliteral{22}{\isachardoublequote}}\ {\isaliteral{5E}{\isacharcircum}}\isanewline
3.1069 +{\isaliteral{22}{\isachardoublequote}}\ \ \ \ \ \ X{\isaliteral{27}{\isacharprime}}\ {\isaliteral{3D}{\isacharequal}}\ Rewrite\ ruleZY\ False\ X{\isaliteral{3B}{\isacharsemicolon}}{\isaliteral{22}{\isachardoublequote}}\ {\isaliteral{5E}{\isacharcircum}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{2A}{\isacharasterisk}}z\ {\isaliteral{2A}{\isacharasterisk}}\ denominator{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{29}{\isacharparenright}}\isanewline
3.1070 +{\isaliteral{22}{\isachardoublequote}}\ \ \ \ \ \ X{\isaliteral{27}{\isacharprime}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}Rewrite{\isaliteral{5F}{\isacharunderscore}}Set\ norm{\isaliteral{5F}{\isacharunderscore}}Rational\ False{\isaliteral{29}{\isacharparenright}}\ X{\isaliteral{27}{\isacharprime}}{\isaliteral{3B}{\isacharsemicolon}}{\isaliteral{22}{\isachardoublequote}}\ {\isaliteral{5E}{\isacharcircum}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{2A}{\isacharasterisk}}simplify{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{29}{\isacharparenright}}\isanewline
3.1071 +{\isaliteral{22}{\isachardoublequote}}\ \ \ \ \ \ funterm\ {\isaliteral{3D}{\isacharequal}}\ rhs\ X{\isaliteral{27}{\isacharprime}}{\isaliteral{22}{\isachardoublequote}}\ {\isaliteral{5E}{\isacharcircum}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{2A}{\isacharasterisk}}drop\ X{\isaliteral{27}{\isacharprime}}{\isaliteral{3D}{\isacharequal}}\ for\ equation\ solving{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{29}{\isacharparenright}}\isanewline
3.1072 +{\isaliteral{22}{\isachardoublequote}}\ \ in\ X{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}\isanewline
3.1073 +\ {\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
3.1074 +{\isaliteral{2A7D}{\isacharverbatimclose}}%
3.1075 +\endisatagML
3.1076 +{\isafoldML}%
3.1077 +%
3.1078 +\isadelimML
3.1079 +%
3.1080 +\endisadelimML
3.1081 +%
3.1082 +\isamarkupsubsection{Check the Program%
3.1083 +}
3.1084 +\isamarkuptrue%
3.1085 +%
3.1086 +\isamarkupsubsubsection{Check the formalization%
3.1087 +}
3.1088 +\isamarkuptrue%
3.1089 +%
3.1090 +\isadelimML
3.1091 +%
3.1092 +\endisadelimML
3.1093 +%
3.1094 +\isatagML
3.1095 +\isacommand{ML}\isamarkupfalse%
3.1096 +\ {\isaliteral{7B2A}{\isacharverbatimopen}}\isanewline
3.1097 +val\ fmz\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{22}{\isachardoublequote}}filterExpression\ {\isaliteral{28}{\isacharparenleft}}X\ \ {\isaliteral{3D}{\isacharequal}}\ {\isadigit{3}}\ {\isaliteral{2F}{\isacharslash}}\ {\isaliteral{28}{\isacharparenleft}}z\ {\isaliteral{2D}{\isacharminus}}\ {\isadigit{1}}{\isaliteral{2F}{\isacharslash}}{\isadigit{4}}\ {\isaliteral{2B}{\isacharplus}}\ {\isaliteral{2D}{\isacharminus}}{\isadigit{1}}{\isaliteral{2F}{\isacharslash}}{\isadigit{8}}\ {\isaliteral{2A}{\isacharasterisk}}\ {\isaliteral{28}{\isacharparenleft}}{\isadigit{1}}{\isaliteral{2F}{\isacharslash}}{\isaliteral{28}{\isacharparenleft}}z{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}real{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\ \isanewline
3.1098 +\ \ {\isaliteral{22}{\isachardoublequote}}stepResponse\ {\isaliteral{28}{\isacharparenleft}}x{\isaliteral{5B}{\isacharbrackleft}}n{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}real{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}bool{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
3.1099 +val\ {\isaliteral{28}{\isacharparenleft}}dI{\isaliteral{2C}{\isacharcomma}}pI{\isaliteral{2C}{\isacharcomma}}mI{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{22}{\isachardoublequote}}Isac{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{22}{\isachardoublequote}}inverse{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{22}{\isachardoublequote}}Z{\isaliteral{5F}{\isacharunderscore}}Transform{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{22}{\isachardoublequote}}SignalProcessing{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{2C}{\isacharcomma}}\ \isanewline
3.1100 +\ \ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{22}{\isachardoublequote}}SignalProcessing{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}{\isaliteral{22}{\isachardoublequote}}Z{\isaliteral{5F}{\isacharunderscore}}Transform{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}{\isaliteral{22}{\isachardoublequote}}inverse{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
3.1101 +\isanewline
3.1102 +val\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{28}{\isacharparenleft}}{\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isadigit{1}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{22}{\isachardoublequote}}{\isaliteral{23}{\isacharhash}}Given{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\ Const\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{22}{\isachardoublequote}}Inverse{\isaliteral{5F}{\isacharunderscore}}Z{\isaliteral{5F}{\isacharunderscore}}Transform{\isaliteral{2E}{\isachardot}}filterExpression{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5F}{\isacharunderscore}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{2C}{\isacharcomma}}\isanewline
3.1103 +\ \ \ \ \ \ \ \ \ \ \ \ {\isaliteral{5B}{\isacharbrackleft}}Const\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{22}{\isachardoublequote}}HOL{\isaliteral{2E}{\isachardot}}eq{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5F}{\isacharunderscore}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{24}{\isachardollar}}\ {\isaliteral{5F}{\isacharunderscore}}\ {\isaliteral{24}{\isachardollar}}\ {\isaliteral{5F}{\isacharunderscore}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{2C}{\isacharcomma}}\isanewline
3.1104 +\ \ \ \ \ \ \ \ \ \ \ {\isaliteral{28}{\isacharparenleft}}{\isadigit{2}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isadigit{1}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{22}{\isachardoublequote}}{\isaliteral{23}{\isacharhash}}Find{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\ Const\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{22}{\isachardoublequote}}Inverse{\isaliteral{5F}{\isacharunderscore}}Z{\isaliteral{5F}{\isacharunderscore}}Transform{\isaliteral{2E}{\isachardot}}stepResponse{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5F}{\isacharunderscore}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{2C}{\isacharcomma}}\isanewline
3.1105 +\ \ \ \ \ \ \ \ \ \ \ \ {\isaliteral{5B}{\isacharbrackleft}}Free\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{22}{\isachardoublequote}}x{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5F}{\isacharunderscore}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{24}{\isachardollar}}\ {\isaliteral{5F}{\isacharunderscore}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{2C}{\isacharcomma}}\isanewline
3.1106 +\ \ \ \ \ \ \ \ \ \ {\isaliteral{5F}{\isacharunderscore}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ prep{\isaliteral{5F}{\isacharunderscore}}ori\ fmz\ thy\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{23}{\isacharhash}}ppc\ o\ get{\isaliteral{5F}{\isacharunderscore}}pbt{\isaliteral{29}{\isacharparenright}}\ pI{\isaliteral{29}{\isacharparenright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
3.1107 +{\isaliteral{2A7D}{\isacharverbatimclose}}%
3.1108 +\endisatagML
3.1109 +{\isafoldML}%
3.1110 +%
3.1111 +\isadelimML
3.1112 +%
3.1113 +\endisadelimML
3.1114 +%
3.1115 +\isamarkupsubsubsection{Stepwise check the program%
3.1116 +}
3.1117 +\isamarkuptrue%
3.1118 +%
3.1119 +\isadelimML
3.1120 +%
3.1121 +\endisadelimML
3.1122 +%
3.1123 +\isatagML
3.1124 +\isacommand{ML}\isamarkupfalse%
3.1125 +\ {\isaliteral{7B2A}{\isacharverbatimopen}}\isanewline
3.1126 +{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2D}{\isacharminus}}{\isaliteral{2D}{\isacharminus}}{\isaliteral{2D}{\isacharminus}}{\isaliteral{2D}{\isacharminus}}{\isaliteral{2D}{\isacharminus}}{\isaliteral{2D}{\isacharminus}}{\isaliteral{2D}{\isacharminus}}{\isaliteral{2D}{\isacharminus}}{\isaliteral{2D}{\isacharminus}}{\isaliteral{2D}{\isacharminus}}{\isaliteral{2D}{\isacharminus}}\ Apply{\isaliteral{5F}{\isacharunderscore}}Method{\isaliteral{3A}{\isacharcolon}}\ exception\ PTREE\ get{\isaliteral{5F}{\isacharunderscore}}obj{\isaliteral{3A}{\isacharcolon}}\ pos\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isadigit{0}}{\isaliteral{5D}{\isacharbrackright}}\ does{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
3.1127 +{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2D}{\isacharminus}}{\isaliteral{2D}{\isacharminus}}{\isaliteral{2D}{\isacharminus}}{\isaliteral{2D}{\isacharminus}}{\isaliteral{2D}{\isacharminus}}{\isaliteral{2D}{\isacharminus}}{\isaliteral{2D}{\isacharminus}}{\isaliteral{2D}{\isacharminus}}{\isaliteral{2D}{\isacharminus}}{\isaliteral{2D}{\isacharminus}}{\isaliteral{2D}{\isacharminus}}\ Apply{\isaliteral{5F}{\isacharunderscore}}Method{\isaliteral{3A}{\isacharcolon}}\ exception\ PTREE\ get{\isaliteral{5F}{\isacharunderscore}}obj{\isaliteral{3A}{\isacharcolon}}\ pos\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isadigit{0}}{\isaliteral{5D}{\isacharbrackright}}\ does{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
3.1128 +{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2D}{\isacharminus}}{\isaliteral{2D}{\isacharminus}}{\isaliteral{2D}{\isacharminus}}{\isaliteral{2D}{\isacharminus}}{\isaliteral{2D}{\isacharminus}}{\isaliteral{2D}{\isacharminus}}{\isaliteral{2D}{\isacharminus}}{\isaliteral{2D}{\isacharminus}}{\isaliteral{2D}{\isacharminus}}{\isaliteral{2D}{\isacharminus}}{\isaliteral{2D}{\isacharminus}}\ Apply{\isaliteral{5F}{\isacharunderscore}}Method{\isaliteral{3A}{\isacharcolon}}\ exception\ PTREE\ get{\isaliteral{5F}{\isacharunderscore}}obj{\isaliteral{3A}{\isacharcolon}}\ pos\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isadigit{0}}{\isaliteral{5D}{\isacharbrackright}}\ does{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
3.1129 +val\ fmz\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{22}{\isachardoublequote}}filterExpression\ {\isaliteral{28}{\isacharparenleft}}X\ z\ {\isaliteral{3D}{\isacharequal}}\ {\isadigit{3}}\ {\isaliteral{2F}{\isacharslash}}\ {\isaliteral{28}{\isacharparenleft}}z\ {\isaliteral{2D}{\isacharminus}}\ {\isadigit{1}}{\isaliteral{2F}{\isacharslash}}{\isadigit{4}}\ {\isaliteral{2B}{\isacharplus}}\ {\isaliteral{2D}{\isacharminus}}{\isadigit{1}}{\isaliteral{2F}{\isacharslash}}{\isadigit{8}}\ {\isaliteral{2A}{\isacharasterisk}}\ {\isaliteral{28}{\isacharparenleft}}{\isadigit{1}}{\isaliteral{2F}{\isacharslash}}{\isaliteral{28}{\isacharparenleft}}z{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}real{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\ \isanewline
3.1130 +\ \ {\isaliteral{22}{\isachardoublequote}}stepResponse\ {\isaliteral{28}{\isacharparenleft}}x{\isaliteral{5B}{\isacharbrackleft}}n{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}real{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}bool{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
3.1131 +val\ {\isaliteral{28}{\isacharparenleft}}dI{\isaliteral{2C}{\isacharcomma}}pI{\isaliteral{2C}{\isacharcomma}}mI{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{22}{\isachardoublequote}}Isac{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{22}{\isachardoublequote}}inverse{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{22}{\isachardoublequote}}Z{\isaliteral{5F}{\isacharunderscore}}Transform{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{22}{\isachardoublequote}}SignalProcessing{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{2C}{\isacharcomma}}\ \isanewline
3.1132 +\ \ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{22}{\isachardoublequote}}SignalProcessing{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}{\isaliteral{22}{\isachardoublequote}}Z{\isaliteral{5F}{\isacharunderscore}}Transform{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}{\isaliteral{22}{\isachardoublequote}}inverse{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
3.1133 +val\ {\isaliteral{28}{\isacharparenleft}}p{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}fb{\isaliteral{2C}{\isacharcomma}}nxt{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}pt{\isaliteral{29}{\isacharparenright}}\ \ {\isaliteral{3D}{\isacharequal}}\ CalcTreeTEST\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{28}{\isacharparenleft}}fmz{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{28}{\isacharparenleft}}dI{\isaliteral{2C}{\isacharcomma}}pI{\isaliteral{2C}{\isacharcomma}}mI{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{3B}{\isacharsemicolon}}\ \isanewline
3.1134 +val\ {\isaliteral{28}{\isacharparenleft}}p{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}fb{\isaliteral{2C}{\isacharcomma}}nxt{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}pt{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ me\ nxt\ p\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ pt{\isaliteral{3B}{\isacharsemicolon}}\isanewline
3.1135 +val\ {\isaliteral{28}{\isacharparenleft}}p{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}fb{\isaliteral{2C}{\isacharcomma}}nxt{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}pt{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ me\ nxt\ p\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ pt{\isaliteral{3B}{\isacharsemicolon}}\isanewline
3.1136 +val\ {\isaliteral{28}{\isacharparenleft}}p{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}fb{\isaliteral{2C}{\isacharcomma}}nxt{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}pt{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ me\ nxt\ p\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ pt{\isaliteral{3B}{\isacharsemicolon}}\isanewline
3.1137 +val\ {\isaliteral{28}{\isacharparenleft}}p{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}fb{\isaliteral{2C}{\isacharcomma}}nxt{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}pt{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ me\ nxt\ p\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ pt{\isaliteral{3B}{\isacharsemicolon}}\isanewline
3.1138 +val\ {\isaliteral{28}{\isacharparenleft}}p{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}fb{\isaliteral{2C}{\isacharcomma}}nxt{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}pt{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ me\ nxt\ p\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ pt{\isaliteral{3B}{\isacharsemicolon}}\isanewline
3.1139 +{\isaliteral{2A7D}{\isacharverbatimclose}}\isanewline
3.1140 +\isacommand{ML}\isamarkupfalse%
3.1141 +\ {\isaliteral{7B2A}{\isacharverbatimopen}}\isanewline
3.1142 +val\ {\isaliteral{28}{\isacharparenleft}}p{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}fb{\isaliteral{2C}{\isacharcomma}}nxt{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}pt{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ me\ nxt\ p\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ pt{\isaliteral{3B}{\isacharsemicolon}}\isanewline
3.1143 +{\isaliteral{2A7D}{\isacharverbatimclose}}\isanewline
3.1144 +\isacommand{ML}\isamarkupfalse%
3.1145 +\ {\isaliteral{7B2A}{\isacharverbatimopen}}\isanewline
3.1146 +val\ {\isaliteral{28}{\isacharparenleft}}p{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}fb{\isaliteral{2C}{\isacharcomma}}nxt{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}pt{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ me\ nxt\ p\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ pt{\isaliteral{3B}{\isacharsemicolon}}\isanewline
3.1147 +{\isaliteral{2A7D}{\isacharverbatimclose}}\isanewline
3.1148 +\isacommand{ML}\isamarkupfalse%
3.1149 +\ {\isaliteral{7B2A}{\isacharverbatimopen}}\isanewline
3.1150 +val\ {\isaliteral{28}{\isacharparenleft}}p{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}fb{\isaliteral{2C}{\isacharcomma}}nxt{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}pt{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ me\ nxt\ p\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ pt{\isaliteral{3B}{\isacharsemicolon}}\isanewline
3.1151 +{\isaliteral{2A7D}{\isacharverbatimclose}}\isanewline
3.1152 +\isacommand{ML}\isamarkupfalse%
3.1153 +\ {\isaliteral{7B2A}{\isacharverbatimopen}}\isanewline
3.1154 +val\ {\isaliteral{28}{\isacharparenleft}}p{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}fb{\isaliteral{2C}{\isacharcomma}}nxt{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}pt{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ me\ nxt\ p\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ pt{\isaliteral{3B}{\isacharsemicolon}}\isanewline
3.1155 +{\isaliteral{2A7D}{\isacharverbatimclose}}\isanewline
3.1156 +\isacommand{ML}\isamarkupfalse%
3.1157 +\ {\isaliteral{7B2A}{\isacharverbatimopen}}\isanewline
3.1158 +val\ {\isaliteral{28}{\isacharparenleft}}p{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}fb{\isaliteral{2C}{\isacharcomma}}nxt{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}pt{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ me\ nxt\ p\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ pt{\isaliteral{3B}{\isacharsemicolon}}\isanewline
3.1159 +{\isaliteral{2A7D}{\isacharverbatimclose}}\isanewline
3.1160 +\isacommand{ML}\isamarkupfalse%
3.1161 +\ {\isaliteral{7B2A}{\isacharverbatimopen}}\isanewline
3.1162 +show{\isaliteral{5F}{\isacharunderscore}}pt\ pt{\isaliteral{3B}{\isacharsemicolon}}\isanewline
3.1163 +{\isaliteral{2A7D}{\isacharverbatimclose}}\isanewline
3.1164 +\isacommand{ML}\isamarkupfalse%
3.1165 +\ {\isaliteral{7B2A}{\isacharverbatimopen}}\isanewline
3.1166 +{\isaliteral{2A7D}{\isacharverbatimclose}}\isanewline
3.1167 +\isacommand{ML}\isamarkupfalse%
3.1168 +\ {\isaliteral{7B2A}{\isacharverbatimopen}}\isanewline
3.1169 +\isanewline
3.1170 +{\isaliteral{2A7D}{\isacharverbatimclose}}\isanewline
3.1171 +\isacommand{ML}\isamarkupfalse%
3.1172 +\ {\isaliteral{7B2A}{\isacharverbatimopen}}\isanewline
3.1173 +\isanewline
3.1174 +{\isaliteral{2A7D}{\isacharverbatimclose}}\isanewline
3.1175 +\isacommand{ML}\isamarkupfalse%
3.1176 +\ {\isaliteral{7B2A}{\isacharverbatimopen}}\isanewline
3.1177 +\isanewline
3.1178 +{\isaliteral{2A7D}{\isacharverbatimclose}}\isanewline
3.1179 +\isacommand{ML}\isamarkupfalse%
3.1180 +\ {\isaliteral{7B2A}{\isacharverbatimopen}}\isanewline
3.1181 +\isanewline
3.1182 +{\isaliteral{2A7D}{\isacharverbatimclose}}\isanewline
3.1183 +\isanewline
3.1184 +\isacommand{ML}\isamarkupfalse%
3.1185 +\ {\isaliteral{7B2A}{\isacharverbatimopen}}\isanewline
3.1186 +\isanewline
3.1187 +{\isaliteral{2A7D}{\isacharverbatimclose}}\isanewline
3.1188 +\isacommand{ML}\isamarkupfalse%
3.1189 +\ {\isaliteral{7B2A}{\isacharverbatimopen}}\isanewline
3.1190 +\isanewline
3.1191 +{\isaliteral{2A7D}{\isacharverbatimclose}}\isanewline
3.1192 +\isanewline
3.1193 +\isacommand{ML}\isamarkupfalse%
3.1194 +\ {\isaliteral{7B2A}{\isacharverbatimopen}}\isanewline
3.1195 +\isanewline
3.1196 +{\isaliteral{2A7D}{\isacharverbatimclose}}\isanewline
3.1197 +\isacommand{ML}\isamarkupfalse%
3.1198 +\ {\isaliteral{7B2A}{\isacharverbatimopen}}\isanewline
3.1199 +\isanewline
3.1200 +{\isaliteral{2A7D}{\isacharverbatimclose}}\isanewline
3.1201 +\isacommand{ML}\isamarkupfalse%
3.1202 +\ {\isaliteral{7B2A}{\isacharverbatimopen}}\isanewline
3.1203 +\isanewline
3.1204 +{\isaliteral{2A7D}{\isacharverbatimclose}}%
3.1205 +\endisatagML
3.1206 +{\isafoldML}%
3.1207 +%
3.1208 +\isadelimML
3.1209 +%
3.1210 +\endisadelimML
3.1211 +%
3.1212 +\isamarkupsection{Write Tests for Crucial Details%
3.1213 +}
3.1214 +\isamarkuptrue%
3.1215 +%
3.1216 +\begin{isamarkuptext}%
3.1217 +===================================%
3.1218 +\end{isamarkuptext}%
3.1219 +\isamarkuptrue%
3.1220 +%
3.1221 +\isadelimML
3.1222 +%
3.1223 +\endisadelimML
3.1224 +%
3.1225 +\isatagML
3.1226 +\isacommand{ML}\isamarkupfalse%
3.1227 +\ {\isaliteral{7B2A}{\isacharverbatimopen}}\isanewline
3.1228 +\isanewline
3.1229 +{\isaliteral{2A7D}{\isacharverbatimclose}}%
3.1230 +\endisatagML
3.1231 +{\isafoldML}%
3.1232 +%
3.1233 +\isadelimML
3.1234 +%
3.1235 +\endisadelimML
3.1236 +%
3.1237 +\isamarkupsection{Integrate Program into Knowledge%
3.1238 +}
3.1239 +\isamarkuptrue%
3.1240 +%
3.1241 +\isadelimML
3.1242 +%
3.1243 +\endisadelimML
3.1244 +%
3.1245 +\isatagML
3.1246 +\isacommand{ML}\isamarkupfalse%
3.1247 +\ {\isaliteral{7B2A}{\isacharverbatimopen}}\isanewline
3.1248 +\isanewline
3.1249 +{\isaliteral{2A7D}{\isacharverbatimclose}}%
3.1250 +\endisatagML
3.1251 +{\isafoldML}%
3.1252 +%
3.1253 +\isadelimML
3.1254 +%
3.1255 +\endisadelimML
3.1256 +\isanewline
3.1257 +%
3.1258 +\isadelimtheory
3.1259 +\isanewline
3.1260 +%
3.1261 +\endisadelimtheory
3.1262 +%
3.1263 +\isatagtheory
3.1264 +\isacommand{end}\isamarkupfalse%
3.1265 +%
3.1266 +\endisatagtheory
3.1267 +{\isafoldtheory}%
3.1268 +%
3.1269 +\isadelimtheory
3.1270 +%
3.1271 +\endisadelimtheory
3.1272 +\isanewline
3.1273 +\isanewline
3.1274 +\end{isabellebody}%
3.1275 +%%% Local Variables:
3.1276 +%%% mode: latex
3.1277 +%%% TeX-master: "root"
3.1278 +%%% End:
4.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
4.2 +++ b/test/Tools/isac/Knowledge/partial_fractions.sml Fri Sep 23 16:22:11 2011 +0200
4.3 @@ -0,0 +1,22 @@
4.4 +(* Title: partial fraction decomposition
4.5 + Author: Jan Rocnik
4.6 + (c) due to copyright terms
4.7 +*)
4.8 +
4.9 +"--------------------------------------------------------";
4.10 +"table of contents --------------------------------------";
4.11 +"--------------------------------------------------------";
4.12 +"----------- get_denominator ----------------------------";
4.13 +"--------------------------------------------------------";
4.14 +"--------------------------------------------------------";
4.15 +"--------------------------------------------------------";
4.16 +
4.17 +
4.18 +"----------- get_denominator ----------------------------";
4.19 +"----------- get_denominator ----------------------------";
4.20 +"----------- get_denominator ----------------------------";
4.21 +val t = @{term "a/(b::real)"};
4.22 +val SOME (str, t') = eval_get_denominator "" 0 t @{theory Isac};
4.23 +if term2str t' = "a / b = b" then () else error "eval_get_denominator";
4.24 +
4.25 +
5.1 --- a/test/Tools/isac/Test_Isac.thy Fri Sep 23 14:56:14 2011 +0200
5.2 +++ b/test/Tools/isac/Test_Isac.thy Fri Sep 23 16:22:11 2011 +0200
5.3 @@ -87,6 +87,7 @@
5.4 ("Knowledge/integrate.sml")
5.5 ("Knowledge/eqsystem.sml")
5.6 ("Knowledge/test.sml")
5.7 + ("Knowledge/partial_fractions.sml")
5.8 ("Knowledge/polyminus.sml")
5.9 ("Knowledge/vect.sml")
5.10 ("Knowledge/diffapp.sml")
5.11 @@ -159,6 +160,7 @@
5.12 (*use "Knowledge/rateq.sml" 2002*)
5.13 (*use "Knowledge/rootrat.sml" 2002*)
5.14 (*use "Knowledge/rootrateq.sml" 2002*)
5.15 + use "Knowledge/partial_fractions.sml"
5.16 (*use "Knowledge/polyeq.sml" part. WN110906: problems with comments*)
5.17 (*use "Knowledge/rlang.sml" 2002???*)
5.18 use "Knowledge/calculus.sml" (*new 2011*)