1 (* Title: partial fraction decomposition
3 (c) due to copyright terms
6 "--------------------------------------------------------";
7 "table of contents --------------------------------------";
8 "--------------------------------------------------------";
9 "----------- why helpless here ? ------------------------";
10 "----------- why not nxt = Model_Problem here ? ---------";
11 "----------- fun factors_from_solution ------------------";
12 "----------- Logic.unvarify_global ----------------------";
13 "----------- eval_drop_questionmarks --------------------";
14 "----------- = me for met_partial_fraction --------------";
15 "----------- autoCalculate for met_partial_fraction -----";
16 "----------- progr.vers.2: check erls for multiply_ansatz";
17 "----------- progr.vers.2: improve program --------------";
18 "--------------------------------------------------------";
19 "--------------------------------------------------------";
20 "--------------------------------------------------------";
23 "----------- why helpless here ? ------------------------";
24 "----------- why helpless here ? ------------------------";
25 "----------- why helpless here ? ------------------------";
26 val fmz = ["filterExpression (X z = 3 / (z - 1/4 + -1/8 * (1/(z::real))))",
27 "stepResponse (x[n::real]::bool)"];
28 val (dI,pI,mI) = ("Isac", ["Inverse", "Z_Transform", "SignalProcessing"],
29 ["SignalProcessing","Z_Transform","Inverse"]);
30 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI,pI,mI))];
31 val (p,_,f,nxt,_,pt) = me nxt p [] pt; "Add_Given";
32 val (p,_,f,nxt,_,pt) = me nxt p [] pt; "Add_Find";
33 val (p,_,f,nxt,_,pt) = me nxt p [] pt; "Specify_Theory";
34 val (p,_,f,nxt,_,pt) = me nxt p [] pt; "Specify_Problem";
35 val (p,_,f,nxt,_,pt) = me nxt p [] pt; "Specify_Method";
36 val (p,_,f,nxt,_,pt) = me nxt p [] pt; "nxt = Apply_Method";
37 val (p,_,f,nxt,_,pt) = me nxt p [] pt; "nxt = Rewrite (ruleZY, Inverse_Z_Transform.ruleZY) --> X z = 3 / (z - 1 / 4 + -1 / 8 * (1 / z))";
38 val (p''',_,f,nxt''',_,pt''') = me nxt p [] pt; "nxt = Rewrite_Set norm_Rational --> X' z = 3 / (z * (z - 1 / 4 + -1 / 8 * (1 / z)))";
39 "~~~~~ fun me, args:"; val ((_,tac), (p:pos'), _, (pt:ctree)) = (nxt, p, [], pt);
40 val ("ok", (_, _, ptp)) = locatetac tac (pt,p)
42 "~~~~~ fun step, args:"; val (((ip as (_,p_)):pos'), ((ptp as (pt,p), tacis):calcstate)) =
43 (p, ((pt, e_pos'),[]));
44 val pIopt = get_pblID (pt,ip);
45 ip = ([],Res); "false";
47 pIopt; (* = SOME ["Inverse", "Z_Transform", "SignalProcessing"]*)
48 member op = [Pbl,Met] p_ andalso is_none (get_obj g_env pt (fst p)); "false";
49 (*nxt_solve_ (pt,ip); "WAS isalist2list applied to NON-list 'no_meth'"
50 THIS MEANS: replace no_meth by [no_meth] in Script.*)
51 (*WAS val ("helpless",_) = step p ((pt, e_pos'),[]) *)
52 (*WAS val (p,_,f,nxt,_,pt) = me nxt p [] pt; "Empty_Tac instead SubProblem";*)
54 "----------- why not nxt = Model_Problem here ? ---------";
55 "----------- why not nxt = Model_Problem here ? ---------";
56 "----------- why not nxt = Model_Problem here ? ---------";
57 val (p,_,f,nxt,_,pt) = me nxt''' p''' [] pt''';
58 "~~~~~ fun me, args:"; val (((_,tac):tac'_), (p:pos'), _, (pt:ctree)) = (nxt, p, c, pt);
59 val ("ok", (_, _, ptp)) = locatetac tac (pt,p);
61 "~~~~~ fun step, args:"; val (((ip as (_,p_)):pos'), ((ptp as (pt,p), tacis):calcstate)) =
62 (p, ((pt, e_pos'),[]));
63 val pIopt = get_pblID (pt,ip);
64 ip = ([],Res); " = false";
66 pIopt (* = SOME ["Inverse", "Z_Transform", "SignalProcessing"]*);
67 member op = [Pbl,Met] p_ andalso is_none (get_obj g_env pt (fst p)); " = false";
68 (* ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ leads into
69 nxt_solve_, which is definitely WRONG (should be nxt_specify_ for FIND_ADD).
70 This ERROR seems to be introduced together with ctxt, concerns Apply_Method without init_form.
74 "----------- fun factors_from_solution ------------------";
75 "----------- fun factors_from_solution ------------------";
76 "----------- fun factors_from_solution ------------------";
77 val ctxt = Proof_Context.init_global @{theory Isac};
78 val SOME t = parseNEW ctxt "factors_from_solution [(z::real) = 1 / 2, z = -1 / 4]";
79 val SOME (_, t') = eval_factors_from_solution "" 0 t thy;
81 "factors_from_solution [z = 1 / 2, z = -1 / 4] = (z - 1 / 2) * (z - -1 / 4)"
82 then () else error "factors_from_solution broken";
84 "----------- Logic.unvarify_global ----------------------";
85 "----------- Logic.unvarify_global ----------------------";
86 "----------- Logic.unvarify_global ----------------------";
87 val A_var = parseNEW ctxt "A::real" |> the |> Logic.varify_global
88 val B_var = parseNEW ctxt "B::real" |> the |> Logic.varify_global
90 val denom1 = parseNEW ctxt "(z + -1 * (1 / 2))::real" |> the;
91 val denom2 = parseNEW ctxt "(z + -1 * (-1 / 4))::real" |> the;
93 val test = HOLogic.mk_binop "Groups.plus_class.plus"
94 (HOLogic.mk_binop "Fields.inverse_class.divide" (A_var, denom1),
95 HOLogic.mk_binop "Fields.inverse_class.divide" (B_var, denom2));
97 if term2str test = "?A / (z + -1 * (1 / 2)) + ?B / (z + -1 * (-1 / 4))" then ()
98 else error "HOLogic.mk_binop broken ?";
100 (* Logic.unvarify_global test
101 ---> exception TERM raised (line 539 of "logic.ML"): Illegal fixed variable: "z"
102 thus we need another fun var2free in termC.sml*)
104 "----------- eval_drop_questionmarks --------------------";
105 "----------- eval_drop_questionmarks --------------------";
106 "----------- eval_drop_questionmarks --------------------";
107 if term2str test = "?A / (z + -1 * (1 / 2)) + ?B / (z + -1 * (-1 / 4))"
108 then () else error "test setup (ctxt!) probably changed";
110 val t = Const ("Partial_Fractions.drop_questionmarks", HOLogic.realT --> HOLogic.realT) $ test;
112 val SOME (_, t') = eval_drop_questionmarks "drop_questionmarks" 0 t @{theory Isac};
113 if term2str t' = "drop_questionmarks (?A / (z + -1 * (1 / 2)) + ?B / (z + -1 * (-1 / 4))) =" ^
114 "\nA / (z + -1 * (1 / 2)) + B / (z + -1 * (-1 / 4))"
115 then () else error "eval_drop_questionmarks broken";
117 "----------- = me for met_partial_fraction --------------";
118 "----------- = me for met_partial_fraction --------------";
119 "----------- = me for met_partial_fraction --------------";
121 ["functionTerm (3 / (z * (z - 1 / 4 + -1 / 8 * (1 / z))))",
122 "solveFor z", "decomposedFunction p_p"];
124 ("Partial_Fractions",
125 ["partial_fraction", "rational", "simplification"],
126 ["simplification","of_rationals","to_partial_fraction"]);
127 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
128 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
129 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
130 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
131 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
132 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
133 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
134 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
135 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
136 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
137 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
138 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
139 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
140 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
141 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
142 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
143 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
144 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
145 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
146 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
147 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
148 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
149 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
150 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
151 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
152 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
153 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
154 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
155 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
156 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
157 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
158 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
159 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
160 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
161 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
162 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
163 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
164 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
165 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
166 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
167 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
168 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
169 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
170 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
171 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
172 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
173 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
174 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
175 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
176 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
177 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
178 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
179 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
180 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
181 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
182 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
183 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
184 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
185 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
186 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
187 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
188 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
189 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
190 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
191 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
192 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
193 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
194 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
195 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
196 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
197 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
198 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
199 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
200 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
201 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
202 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
203 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
204 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
205 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
206 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
207 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
208 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
209 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
210 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
211 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
212 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
213 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
214 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
215 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
216 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
217 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
218 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
219 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
222 if f2str f = "4 / (z - 1 / 2) + -4 / (z - -1 / 4)" then()
223 else error "= me .. met_partial_fraction broken";
225 "----------- autoCalculate for met_partial_fraction -----";
226 "----------- autoCalculate for met_partial_fraction -----";
227 "----------- autoCalculate for met_partial_fraction -----";
230 ["functionTerm (3 / (z * (z - 1 / 4 + -1 / 8 * (1 / z))))",
231 "solveFor z", "decomposedFunction p_p"];
232 val (dI', pI', mI') =
233 ("Partial_Fractions",
234 ["partial_fraction", "rational", "simplification"],
235 ["simplification","of_rationals","to_partial_fraction"]);
236 CalcTree [(fmz, (dI' ,pI' ,mI'))];
239 autoCalculate 1 CompleteCalc;
241 val ((pt,p),_) = get_calc 1; val ip = get_pos 1 1;
242 if p = ip andalso ip = ([], Res) then ()
243 else error "autoCalculate for met_partial_fraction changed: final pos'";
245 val (Form f, tac, asms) = pt_extract (pt, p);
246 if term2str f = "4 / (z - 1 / 2) + -4 / (z - -1 / 4)" andalso
247 terms2str' asms = "[~ matches (?a = 0) (3 = -3 * B / 4) | ~ lhs (3 = -3 * B / 4) is_poly_in B," ^
248 "B = -4,lhs (3 + 3 / 4 * B = 0) is_poly_in B,lhs (3 + 3 / 4 * B = 0) has_degree_in B = 1," ^
249 "B is_polyexp,A is_polyexp," ^
250 "~ matches (?a = 0) (3 = 3 * A / 4) | ~ lhs (3 = 3 * A / 4) is_poly_in A," ^
251 "A = 4,lhs (3 + -3 / 4 * A = 0) is_poly_in A,lhs (3 + -3 / 4 * A = 0) has_degree_in A = 1," ^
252 "lhs (-1 + -2 * z + 8 * z ^^^ 2 = 0) has_degree_in z = 2," ^
253 "lhs (-1 + -2 * z + 8 * z ^^^ 2 = 0) is_poly_in z,z = 1 / 2,z = -1 / 4,z is_polyexp]"
254 then case tac of NONE => ()
255 | _ => error "autoCalculate for met_partial_fraction changed: final result 1"
256 else error "autoCalculate for met_partial_fraction changed: final result 2"
260 (([], Frm), Problem (Partial_Fractions, [partial_fraction, rational, simplification])),
261 (([1], Frm), 3 / (z * (z - 1 / 4 + -1 / 8 * (1 / z)))),
262 (([1], Res), 24 / (-1 + -2 * z + 8 * z ^^^ 2)),
263 (([2], Pbl), solve (-1 + -2 * z + 8 * z ^^^ 2 = 0, z)),
264 (([2,1], Frm), -1 + -2 * z + 8 * z ^^^ 2 = 0),
265 (([2,1], Res), z = (- -2 + sqrt (-2 ^^^ 2 - 4 * 8 * -1)) / (2 * 8) |
266 z = (- -2 - sqrt (-2 ^^^ 2 - 4 * 8 * -1)) / (2 * 8)),
267 (([2,2], Res), z = 1 / 2 | z = -1 / 4),
268 (([2,3], Res), [z = 1 / 2, z = -1 / 4]),
269 (([2,4], Res), [z = 1 / 2, z = -1 / 4]),
270 (([2], Res), [z = 1 / 2, z = -1 / 4]),
271 (([3], Frm), 3 / ((z - 1 / 2) * (z - -1 / 4))),
272 (([3], Res), ?A / (z - 1 / 2) + ?B / (z - -1 / 4)),
273 (([4], Frm), 3 / ((z - 1 / 2) * (z - -1 / 4)) = ?A / (z - 1 / 2) + ?B / (z - -1 / 4)),
274 (([4], Res), 3 = ?A * (z - -1 / 4) + ?B * (z - 1 / 2)),
275 (([5], Frm), 3 = A * (z - -1 / 4) + B * (z - 1 / 2)),
276 (([5], Res), 3 = A * (1 / 2 - -1 / 4) + B * (1 / 2 - 1 / 2)),
277 (([6], Res), 3 = 3 * A / 4),
278 (([7], Pbl), solve (3 = 3 * A / 4, A)),
279 (([7,1], Frm), 3 = 3 * A / 4),
280 (([7,1], Res), 3 - 3 * A / 4 = 0),
281 (([7,2], Res), 3 / 1 + -3 / 4 * A = 0),
282 (([7,3], Res), 3 + -3 / 4 * A = 0),
283 (([7,4], Pbl), solve (3 + -3 / 4 * A = 0, A)),
284 (([7,4,1], Frm), 3 + -3 / 4 * A = 0),
285 (([7,4,1], Res), A = -1 * 3 / (-3 / 4)),
286 (([7,4,2], Res), A = -3 / (-3 / 4)),
287 (([7,4,3], Res), A = 4),
288 (([7,4,4], Res), [A = 4]),
289 (([7,4,5], Res), [A = 4]),
290 (([7,4], Res), [A = 4]),
291 (([7], Res), [A = 4]),
292 (([8], Frm), 3 = A * (z - -1 / 4) + B * (z - 1 / 2)),
293 (([8], Res), 3 = A * (-1 / 4 - -1 / 4) + B * (-1 / 4 - 1 / 2)),
294 (([9], Res), 3 = -3 * B / 4),
295 (([10], Pbl), solve (3 = -3 * B / 4, B)),
296 (([10,1], Frm), 3 = -3 * B / 4),
297 (([10,1], Res), 3 - -3 * B / 4 = 0),
298 (([10,2], Res), 3 / 1 + 3 / 4 * B = 0),
299 (([10,3], Res), 3 + 3 / 4 * B = 0),
300 (([10,4], Pbl), solve (3 + 3 / 4 * B = 0, B)),
301 (([10,4,1], Frm), 3 + 3 / 4 * B = 0),
302 (([10,4,1], Res), B = -1 * 3 / (3 / 4)),
303 (([10,4,2], Res), B = -3 / (3 / 4)),
304 (([10,4,3], Res), B = -4),
305 (([10,4,4], Res), [B = -4]),
306 (([10,4,5], Res), [B = -4]),
307 (([10,4], Res), [B = -4]),
308 (([10], Res), [B = -4]),
309 (([11], Frm), A / (z - 1 / 2) + B / (z - -1 / 4)),
310 (([11], Res), 4 / (z - 1 / 2) + -4 / (z - -1 / 4)),
311 (([], Res), 4 / (z - 1 / 2) + -4 / (z - -1 / 4))] *)
313 "----------- progr.vers.2: check erls for multiply_ansatz";
314 "----------- progr.vers.2: check erls for multiply_ansatz";
315 "----------- progr.vers.2: check erls for multiply_ansatz";
316 (*test for outcommented 3 lines in script: is norm_Rational strong enough?*)
317 val t = str2term "(3 / ((-1 + -2 * z + 8 * z ^^^ 2) *3/24)) = (3 / ((z - 1 / 2) * (z - -1 / 4)))";
318 val SOME (t', _) = rewrite_set_ @{theory Isac} true ansatz_rls t;
319 term2str t' = "3 / ((-1 + -2 * z + 8 * z ^^^ 2) * 3 / 24) =\n?A / (z - 1 / 2) + ?B / (z - -1 / 4)";
321 val SOME (t'', _) = rewrite_set_ @{theory Isac} true multiply_ansatz t'; (*true*)
322 term2str t'' = "(z - 1 / 2) * (z - -1 / 4) * 3 / ((-1 + -2 * z + 8 * z ^^^ 2) * 3 / 24) =\n" ^
323 "?A * (z - -1 / 4) + ?B * (z - 1 / 2)"; (*true*)
325 val SOME (t''', _) = rewrite_set_ @{theory Isac} true norm_Rational t'';
326 if term2str t''' = "3 = ?A * (1 + 4 * z) / 4 + ?B * (-1 + 2 * z) / 2" then ()
327 else error "ansatz_rls - multiply_ansatz - norm_Rational broken";
329 (*test for outcommented 3 lines in script: empower erls for x = a*b ==> ...*)
330 val xxx = append_rls "multiply_ansatz_erls" norm_Rational
331 [Calc ("HOL.eq",eval_equal "#equal_")];
333 val multiply_ansatz = prep_rls @{theory} (
334 Rls {id = "multiply_ansatz", preconds = [], rew_ord = ("dummy_ord",dummy_ord),
336 srls = Erls, calc = [], errpatts = [],
338 [Thm ("multiply_2nd_order",num_str @{thm multiply_2nd_order})
340 scr = EmptyScr}:rls);
342 rewrite_set_ thy true xxx @{term "a+b = a+(b::real)"}; (*SOME ok*)
343 rewrite_set_ thy true multiply_ansatz @{term "a+b = a+(b::real)"}; (*why NONE?: GOON*)
345 "----------- progr.vers.2: improve program --------------";
346 "----------- progr.vers.2: improve program --------------";
347 "----------- progr.vers.2: improve program --------------";
348 (*WN120318 stopped due to much effort with the test above*)
349 "Script PartFracScript (f_f::real) (zzz::real) = " ^(*f_f: 3 / (z * (z - 1 / 4 + -1 / 8 * (1 / z)), zzz: z*)
350 " (let f_f = Take f_f; " ^
351 " (num_orig::real) = get_numerator f_f; " ^(*num_orig: 3*)
352 " f_f = (Rewrite_Set norm_Rational False) f_f; " ^(*f_f: 24 / (-1 + -2 * z + 8 * z ^^^ 2)*)
353 " (numer::real) = get_numerator f_f; " ^(*numer: 24*)
354 " (denom::real) = get_denominator f_f; " ^(*denom: -1 + -2 * z + 8 * z ^^^ 2*)
355 " (equ::bool) = (denom = (0::real)); " ^(*equ: -1 + -2 * z + 8 * z ^^^ 2 = 0*)
356 " (L_L::bool list) = (SubProblem (PolyEq', " ^
357 " [abcFormula, degree_2, polynomial, univariate, equation], " ^
358 " [no_met]) [BOOL equ, REAL zzz]); " ^(*L_L: [z = 1 / 2, z = -1 / 4]*)
359 " (facs::real) = factors_from_solution L_L; " ^(*facs: (z - 1 / 2) * (z - -1 / 4)*)
360 " (eql::real) = Take (num_orig / facs); " ^(*eql: 3 / ((z - 1 / 2) * (z - -1 / 4)) *)
361 " (eqr::real) = (Try (Rewrite_Set ansatz_rls False)) eql; " ^(*eqr: ?A / (z - 1 / 2) + ?B / (z - -1 / 4)*)
362 " (eq::bool) = Take (eql = eqr); " ^(*eq: 3 / ((z - 1 / 2) * (z - -1 / 4)) = ?A / (z - 1 / 2) + ?B / (z - -1 / 4)*)
363 (*this has been tested below by rewrite_set_
364 " (eeeee::bool) = Take ((num_orig / denom * denom / numer) = (num_orig / facs));" ^(**)
365 " (eeeee::bool) = (Rewrite_Set ansatz_rls False) eeeee;" ^(**)
366 " eq = (Try (Rewrite_Set multiply_ansatz False)) eeeee; " ^(*eq: 3 = ?A * (z - -1 / 4) + ?B * (z - 1 / 2)*)
367 NEXT try to outcomment the very next line..*)
368 " eq = (Try (Rewrite_Set equival_trans False)) eeeee; " ^(*eq: 3 = ?A * (z - -1 / 4) + ?B * (z - 1 / 2)*)
369 " eq = drop_questionmarks eq; " ^(*eq: 3 = A * (z - -1 / 4) + B * (z - 1 / 2)*)
370 " (z1::real) = (rhs (NTH 1 L_L)); " ^(*z1: 1 / 2*)
371 " (z2::real) = (rhs (NTH 2 L_L)); " ^(*z2: -1 / 4*)
372 " (eq_a::bool) = Take eq; " ^(*eq_a: 3 = A * (z - -1 / 4) + B * (z - 1 / 2)*)
373 " eq_a = (Substitute [zzz = z1]) eq; " ^(*eq_a: 3 = A * (1 / 2 - -1 / 4) + B * (1 / 2 - 1 / 2)*)
374 " eq_a = (Rewrite_Set norm_Rational False) eq_a; " ^(*eq_a: 3 = 3 * A / 4*)
375 " (sol_a::bool list) = " ^
376 " (SubProblem (Isac', [univariate,equation], [no_met]) " ^
377 " [BOOL eq_a, REAL (A::real)]); " ^(*sol_a: [A = 4]*)
378 " (a::real) = (rhs (NTH 1 sol_a)); " ^(*a: 4*)
379 " (eq_b::bool) = Take eq; " ^(*eq_b: 3 = A * (z - -1 / 4) + B * (z - 1 / 2)*)
380 " eq_b = (Substitute [zzz = z2]) eq_b; " ^(*eq_b: *)
381 " eq_b = (Rewrite_Set norm_Rational False) eq_b; " ^(*eq_b: *)
382 " (sol_b::bool list) = " ^
383 " (SubProblem (Isac', [univariate,equation], [no_met]) " ^
384 " [BOOL eq_b, REAL (B::real)]); " ^(*sol_b: [B = -4]*)
385 " (b::real) = (rhs (NTH 1 sol_b)); " ^(*b: -4*)
386 " eqr = drop_questionmarks eqr; " ^(*eqr: A / (z - 1 / 2) + B / (z - -1 / 4)*)
387 " (pbz::real) = Take eqr; " ^(*pbz: A / (z - 1 / 2) + B / (z - -1 / 4)*)
388 " pbz = ((Substitute [A = a, B = b]) pbz) " ^(*pbz: 4 / (z - 1 / 2) + -4 / (z - -1 / 4)*)