1 (* testexamples for RootratEq, equations mixing fractions and roots
2 WN120314 some complicated equations still are outcommented.
5 "-----------------------------------------------------------------";
6 "table of contents -----------------------------------------------";
7 "-----------------------------------------------------------------";
8 "------------ tests on predicates -------------------------------";
9 "------------ test thm rootrat_equation_left_1 -------------------";
10 "------------ test thm rootrat_equation_left_2 -------------------";
11 "------------ test thm rootrat_equation_right_1 ------------------";
12 "------------ test thm rootrat_equation_right_2 ------------------";
13 "-----------------------------------------------------------------";
14 "-----------------------------------------------------------------";
16 val thy = @{theory "RootRatEq"};
18 "------------ tests on predicates -------------------------------";
19 "------------ tests on predicates -------------------------------";
20 "------------ tests on predicates -------------------------------";
21 val t1 = (Thm.term_of o the o (parse thy)) "(-8 - sqrt(x) + x^^^2) is_rootRatAddTerm_in x";
22 val SOME (t,_) = rewrite_set_ @{theory "RootRatEq"} false RootRatEq_prls t1;
23 if (term2str t) = "False" then ()
24 else error "rootrateq.sml: diff.behav. 1 in is_rootRatAddTerm_in";
26 val t1 = (Thm.term_of o the o (parse thy)) "(1/x) is_rootRatAddTerm_in x";
27 val SOME (t,_) = rewrite_set_ @{theory "RootRatEq"} false RootRatEq_prls t1;
28 if (term2str t) = "False" then ()
29 else error "rootrateq.sml: diff.behav. 2 in is_rootRatAddTerm_in";
31 val t1 = (Thm.term_of o the o (parse thy)) "(1/sqrt(x)) is_rootRatAddTerm_in x";
32 val SOME (t,_) = rewrite_set_ @{theory "RootRatEq"} false RootRatEq_prls t1;
33 if (term2str t) = "False" then ()
34 else error "rootrateq.sml: diff.behav. 3 in is_rootRatAddTerm_in";
36 val t1 = (Thm.term_of o the o (parse thy)) "(1/(sqrt(x)+1)) is_rootRatAddTerm_in x";
37 val SOME (t,_) = rewrite_set_ @{theory "RootRatEq"} false RootRatEq_prls t1;
38 if (term2str t) = "True" then ()
39 else error "rootrateq.sml: diff.behav. 4 in is_rootRatAddTerm_in";
41 val t1 = (Thm.term_of o the o (parse thy)) "(3 + 1/(1+sqrt(x))) is_rootRatAddTerm_in x";
42 val SOME (t,_) = rewrite_set_ @{theory "RootRatEq"} false RootRatEq_prls t1;
43 if (term2str t) = "True" then ()
44 else error "rootrateq.sml: diff.behav. 5 in is_rootRatAddTerm_in";
46 val t1 = (Thm.term_of o the o (parse thy)) "(1/(1+sqrt(y)) + 3 + 1/(1+sqrt(x))) is_rootRatAddTerm_in x";
47 val SOME (t,_) = rewrite_set_ @{theory "RootRatEq"} false RootRatEq_prls t1;
48 if (term2str t) = "True" then ()
49 else error "rootrateq.sml: diff.behav. 6 in is_rootRatAddTerm_in";
51 val t1 = (Thm.term_of o the o (parse thy)) "(1/(1+sqrt(x)) + 3 + 1/(1+sqrt(y))) is_rootRatAddTerm_in x";
52 val SOME (t,_) = rewrite_set_ @{theory "RootRatEq"} false RootRatEq_prls t1;
53 if (term2str t) = "True" then ()
54 else error "rootrateq.sml: diff.behav. 7 in is_rootRatAddTerm_in";
56 "------------ test thm rootrat_equation_left_1 -------------------";
57 "------------ test thm rootrat_equation_left_1 -------------------";
58 "------------ test thm rootrat_equation_left_1 -------------------";
60 val fmz = ["equality ( -2 + 1/(1 - sqrt(x))= (0::real))", "solveFor x","solutions L"];
61 val (dI',pI',mI') = ("RootRatEq",["univariate","equation"],["no_met"]);
62 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
63 val (p,_,f,nxt,_,pt) = me nxt p c pt;
64 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
65 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
66 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
67 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
68 val (p,_,f,nxt,_,pt) = me nxt p c pt;
69 (*============ inhibit exn WN120319 ==============================================
70 (*From final Test_Isac.thy we suddenly have
72 nxt = ("Model_Problem", Model_Problem)
74 which we did not investigate further due to the decision to drop the whole type of equation.
76 if f2str f = "1 = (0 - -2) * (1 + -1 * sqrt x)" then ()
77 else error "rootrateq.sml: diff.behav. in rootrat_equation_left_1 a";
78 (*-> Subproblem ("RootRatEq", ["sq", "rootX", "univariate", "equation"])*)
79 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
80 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
81 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
82 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
83 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p''',_,f,nxt,_,pt''') = me nxt p c pt;
85 (*we investigate, why the next step results in Empty_Tac*)
86 f2str f = "1 = 2 * (1 + -1 * sqrt x)";
87 nxt = ("Rewrite_Set", Rewrite_Set "make_rooteq");
88 (*... these ar the step's arguments; from these we do directly ...*)
89 val SOME t = parseNEW ctxt "1 = 2 * (1 + -1 * sqrt x)"
90 val SOME (t, _) = rewrite_set_ thy true make_rooteq t;
91 term2str t = "1 = 2 + -2 * sqrt x";
92 (*... which works; thus error must be in script interpretation*)
94 "~~~~~ fun me, args:"; val (((_,tac):tac'_), (p:pos'), _, (pt:ctree)) = (nxt, p, c, pt);
95 val (pt, p) = case locatetac tac (pt,p) of
96 ("ok", (_, _, ptp)) => ptp;
97 "~~~~~ fun step, args:"; val (ip as (_,p_), (ptp as (pt,p), tacis)) = (p, ((pt, e_pos'), []))
98 val pIopt = get_pblID (pt,ip);
99 ip; (*= ([3, 2], Res)*)
101 pIopt; (*= SOME ["sq", "rootX", "univariate", "equation"]*)
102 member op = [Pbl,Met] p_ andalso is_none (get_obj g_env pt (fst p)); (*= false*)
103 "~~~~~ fun nxt_solve_, args:"; (*stopped due to strange exn
104 "check_elementwise: no set 1 = 2 + -2 * sqrt x"*)
106 (*---- 2nd try: we investigate the script ["RootEq","solve_sq_root_equation"] found via pbl*)
107 val t = str2term "((lhs e_e) is_sqrtTerm_in v_v) | ((rhs e_e) is_sqrtTerm_in v_v)";
108 val t = str2term ("((lhs (1 = 2 * (1 + -1 * sqrt x))) is_sqrtTerm_in x) |" ^
109 " ((rhs (1 = 2 * (1 + -1 * sqrt x))) is_sqrtTerm_in x)");
110 val SOME (t, _) = rewrite_set_ thy true rooteq_srls t;
111 term2str t = "True | True"; (*...was same in 2002 (NOT "True"); so program seems to take
112 [univariate,equation] and to refine to ["sq", "rootX", "univariate", "equation"] in 2002*)
114 (*(*these are the errors during stepping into the code:*)
115 nxt_solve_ (pt,ip); (*check_elementwise: no set 1 = 2 + -2 * sqrt x: fun mk_set raises
116 this exn in Check_elementwise ONLY ?!?*)
117 step p ((pt, e_pos'),[]); (* = ("helpless",*)
120 val (p,_,f,nxt,_,pt) = me nxt p''' c pt''';
121 f2str f = "1 = 2 + -2 * sqrt x)"; (* <<<-------------- this should be*)
122 fst nxt = "Empty_Tac"; (* <<<-------------- this we have*)
123 (*============ inhibit exn WN120314: stopped due to effort; continue with equ-solver
124 The equation is strange: it calls script ["RootEq","solve_sq_root_equation"] twice
125 and works differently due to an "if" in that script.
127 if f2str f = "1 = 2 + -2 * sqrt x" then ()
128 else error "rootrateq.sml: diff.behav. in rootrat_equation_left_1 b";
129 (*-> Subproblem ("RootRatEq", ["sq", "rootX", "univariate", "equation"]) ?!? the SAME as above*)
130 val (p,_,f,nxt,_,pt) = me nxt p c pt;
131 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
132 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
133 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
134 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
135 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
136 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
137 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
138 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
139 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
140 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
141 if f2str f = "1 = 4 * x" then ()
142 else error "rootrateq.sml: diff.behav. in rootrat_equation_left_1 c";
143 (*-> Subproblem ("PolyEq", ["normalise", "polynomial", "univariate", "equation"])*)
144 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
145 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
146 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
147 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
148 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
149 val (p,_,f,nxt,_,pt) = me nxt p c pt;
150 if f2str f = "1 + -4 * x = 0" then ()
151 else error "rootrateq.sml: diff.behav. in rootrat_equation_left_1";
152 (*-> Subproblem ("PolyEq", ["degree_1", "polynomial", "univariate", "equation"])*)
153 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
154 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
155 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
156 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
157 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
158 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
159 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
160 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
161 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
162 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
163 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 1 / 4]")) => ()
164 | _ => error "rootrateq.sml: diff.behav. in -2 + 1/(1 - sqrt(x))= 0 -> [x = 1/4]";
165 ============ inhibit exn WN120314 ==============================================*)
166 ============ inhibit exn WN120319 ==============================================*)
168 "------------ test thm rootrat_equation_left_2 -------------------";
169 "------------ test thm rootrat_equation_left_2 -------------------";
170 "------------ test thm rootrat_equation_left_2 -------------------";
171 val fmz = ["equality (3/(1+sqrt(x))= 1)", "solveFor x","solutions L"];
172 val (dI',pI',mI') = ("RootRatEq",["univariate","equation"],["no_met"]);
174 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
175 val (p,_,f,nxt,_,pt) = me nxt p c pt;
176 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
177 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
178 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
179 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
180 (*-> Subproblem ("RootEq", ["univariate", ...])*)
181 val (p,_,f,nxt,_,pt) = me nxt p c pt;
182 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
183 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
184 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
185 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
186 val (p,_,f,nxt,_,pt) = me nxt p c pt;
187 (*-> Subproblem ("RootEq", ["univariate", ...])*)
188 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
189 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
190 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
191 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
192 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
193 val (p,_,f,nxt,_,pt) = me nxt p c pt;
194 (*-> Subproblem ("RootEq", ["univariate", ...])*)
195 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
196 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
197 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
198 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
199 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
200 val (p,_,f,nxt,_,pt) = me nxt p c pt;
201 (*============ inhibit exn WN120314 ==============================================
202 if f = Form' (FormKF (~1, EdUndef, 0, Nundef, "4 + -1 * x = 0")) then ()
203 else error "rootrateq.sml: diff.behav. in rootrat_equation_left_2";
204 (*-> Subproblem ("PolyEq", ["polynomial", ...])*)
205 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
206 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
207 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
208 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
209 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
210 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
211 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
212 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
213 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
214 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
215 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 4]")) => ()
216 | _ => error "rootrateq.sml: diff.behav. in 3/(1+sqrt(x))= 1 -> [x = 4]";
217 ============ inhibit exn WN120314 ==============================================*)
219 "------------ test thm rootrat_equation_right_1 ------------------";
220 "------------ test thm rootrat_equation_right_1 ------------------";
221 "------------ test thm rootrat_equation_right_1 ------------------";
222 val fmz = ["equality ( 0= -2 + 1/(1 - sqrt(x)))", "solveFor x","solutions L"];
223 val (dI',pI',mI') = ("RootRatEq",["univariate","equation"],["no_met"]);
225 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
226 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
227 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
228 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
229 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
230 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
231 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
232 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
233 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
234 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
235 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
236 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
237 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
238 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
239 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
240 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
241 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
242 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
243 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
244 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
245 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
246 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
247 val (p,_,f,nxt,_,pt) = me nxt p c pt;
248 (*============ inhibit exn WN120314: similar complicated equation, dropped.
249 if f = Form' (FormKF (~1, EdUndef, 0, Nundef, "-1 + 4 * x = 0")) then ()
250 else error "rootrateq.sml: diff.behav.ppoly in rootrat_equation_right_1";
251 val (p,_,f,nxt,_,pt) = me nxt p c pt;
252 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
253 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
254 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
255 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
256 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
257 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
258 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
259 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
260 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
261 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
262 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 1 / 4]")) => ()
263 | _ => error "rootrateq.sml: diff.behav. in -2 + 1/(1 - sqrt(x))= 0 -> [x = 1/4]";
264 ============ inhibit exn WN120314 ==============================================*)
266 "------------ test thm rootrat_equation_right_2 ------------------";
267 "------------ test thm rootrat_equation_right_2 ------------------";
268 "------------ test thm rootrat_equation_right_2 ------------------";
269 val fmz = ["equality (1 = 3/(1+sqrt(x)))", "solveFor x","solutions L"];
270 val (dI',pI',mI') = ("RootRatEq",["univariate","equation"],["no_met"]);
272 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
273 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
274 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
275 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
276 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
277 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
278 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
279 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
280 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
281 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
282 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
283 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
284 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
285 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
286 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
287 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
288 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
289 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
290 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
291 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
292 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
293 val (p,_,f,nxt,_,pt) = me nxt p c pt;
294 (*============ inhibit exn WN120314 ==============================================
295 if f = Form' (FormKF (~1, EdUndef, 0, Nundef, "-4 + x = 0")) then ()
296 else error "rootrateq.sml: diff.behav. in rootrat_equation_right_2";
297 val (p,_,f,nxt,_,pt) = me nxt p c pt;
298 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
299 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
300 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
301 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
302 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
303 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
304 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
305 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
306 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
307 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
308 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 4]")) => ()
309 | _ => error "rootrateq.sml: diff.behav. in 3/(1+sqrt(x))= 1 -> [x = 4]";
310 ============ inhibit exn WN120314 ==============================================*)