intermed. test/../biegelinie.sml
+ meeting dmeindl: Rational2.thy
1 (* chapter 'Biegelinie' from the textbook:
2 Timischl, Kaiser. Ingenieur-Mathematik 3. Wien 1999. p.268-271.
3 author: Walther Neuper 050826,
4 (c) due to copyright terms
7 theory Biegelinie imports Integrate Equation EqSystem Atools begin
11 qq :: "real => real" (* Streckenlast *)
12 Q :: "real => real" (* Querkraft *)
13 Q' :: "real => real" (* Ableitung der Querkraft *)
14 M'_b :: "real => real" ("M'_b") (* Biegemoment *)
15 M'_b' :: "real => real" ("M'_b'") (* Ableitung des Biegemoments *)
16 y'' :: "real => real" (* 2.Ableitung der Biegeline *)
17 y' :: "real => real" (* Neigung der Biegeline *)
18 (*y :: "real => real" (* Biegeline *)*)
19 EI :: "real" (* Biegesteifigkeit *)
21 (*new Descriptions in the related problems*)
22 Traegerlaenge :: "real => una"
23 Streckenlast :: "real => una"
24 BiegemomentVerlauf :: "bool => una"
25 Biegelinie :: "(real => real) => una"
26 Randbedingungen :: "bool list => una"
27 RandbedingungenBiegung :: "bool list => una"
28 RandbedingungenNeigung :: "bool list => una"
29 RandbedingungenMoment :: "bool list => una"
30 RandbedingungenQuerkraft :: "bool list => una"
31 FunktionsVariable :: "real => una"
32 Funktionen :: "bool list => una"
33 Gleichungen :: "bool list => una"
36 Biegelinie2Script :: "[real,real,real,real=>real,bool list,
38 ("((Script Biegelinie2Script (_ _ _ _ _ =))// (_))" 9)
39 BiegelinieScript :: "[real,real,real,real=>real,bool list,bool list,
41 ("((Script BiegelinieScript (_ _ _ _ _ _ =))// (_))" 9)
42 Biege2xIntegrierenScript :: "[real,real,real,bool,real=>real,bool list,
44 ("((Script Biege2xIntegrierenScript (_ _ _ _ _ _ =))// (_))" 9)
45 Biege4x4SystemScript :: "[real,real,real,real=>real,bool list,
47 ("((Script Biege4x4SystemScript (_ _ _ _ _ =))// (_))" 9)
48 Biege1xIntegrierenScript ::
49 "[real,real,real,real=>real,bool list,bool list,bool list,
51 ("((Script Biege1xIntegrierenScript (_ _ _ _ _ _ _ =))// (_))" 9)
52 Belastung2BiegelScript :: "[real,real,
53 bool list] => bool list"
54 ("((Script Belastung2BiegelScript (_ _ =))// (_))" 9)
55 SetzeRandbedScript :: "[bool list,bool list,
56 bool list] => bool list"
57 ("((Script SetzeRandbedScript (_ _ =))// (_))" 9)
59 axioms(*axiomatization where*)
61 Querkraft_Belastung: "Q' x = -qq x" (*and*)
62 Belastung_Querkraft: "-qq x = Q' x" (*and*)
64 Moment_Querkraft: "M_b' x = Q x" (*and*)
65 Querkraft_Moment: "Q x = M_b' x" (*and*)
67 Neigung_Moment: "y'' x = -M_b x/ EI" (*and*)
68 Moment_Neigung: "M_b x = -EI * y'' x" (*and*)
70 (*according to rls 'simplify_Integral': .. = 1/a * .. instead .. = ../ a*)
71 make_fun_explicit: "Not (a =!= 0) ==> (a * (f x) = b) = (f x = 1/a * b)"
76 (** theory elements for transfer into html **)
78 store_isa ["IsacKnowledge"] [];
80 ["Walther Neuper 2005 supported by a grant from NMI Austria"];
81 store_isa ["IsacKnowledge", theory2thyID thy, "Theorems"]
82 ["Walther Neuper 2005 supported by a grant from NMI Austria"];
83 store_thm thy ("Belastung_Querkraft", prop_of @{thm Belastung_Querkraft})
84 ["Walther Neuper 2005 supported by a grant from NMI Austria"];
85 store_thm thy ("Moment_Neigung", prop_of @{thm Moment_Neigung})
86 ["Walther Neuper 2005 supported by a grant from NMI Austria"];
87 store_thm thy ("Moment_Querkraft", prop_of @{thm Moment_Querkraft})
88 ["Walther Neuper 2005 supported by a grant from NMI Austria"];
89 store_thm thy ("Neigung_Moment", prop_of @{thm Neigung_Moment})
90 ["Walther Neuper 2005 supported by a grant from NMI Austria"];
91 store_thm thy ("Querkraft_Belastung", prop_of @{thm Querkraft_Belastung})
92 ["Walther Neuper 2005 supported by a grant from NMI Austria"];
93 store_thm thy ("Querkraft_Moment", prop_of @{thm Querkraft_Moment})
94 ["Walther Neuper 2005 supported by a grant from NMI Austria"];
95 store_thm thy ("make_fun_explicit", prop_of @{thm make_fun_explicit})
96 ["Walther Neuper 2005 supported by a grant from NMI Austria"];
103 (prep_pbt thy "pbl_bieg" [] e_pblID
105 [("#Given" ,["Traegerlaenge l_l", "Streckenlast q_q"]),
106 (*("#Where",["0 < l_l"]), ...wait for < and handling Arbfix*)
107 ("#Find" ,["Biegelinie b_b"]),
108 ("#Relate",["Randbedingungen r_b"])
110 append_rls "e_rls" e_rls [],
112 [["IntegrierenUndKonstanteBestimmen2"]]));
115 (prep_pbt thy "pbl_bieg_mom" [] e_pblID
116 (["MomentBestimmte","Biegelinien"],
117 [("#Given" ,["Traegerlaenge l_l", "Streckenlast q_q"]),
118 (*("#Where",["0 < l_l"]), ...wait for < and handling Arbfix*)
119 ("#Find" ,["Biegelinie b_b"]),
120 ("#Relate",["RandbedingungenBiegung r_b","RandbedingungenMoment r_m"])
122 append_rls "e_rls" e_rls [],
124 [["IntegrierenUndKonstanteBestimmen"]]));
127 (prep_pbt thy "pbl_bieg_momg" [] e_pblID
128 (["MomentGegebene","Biegelinien"],
130 append_rls "e_rls" e_rls [],
132 [["IntegrierenUndKonstanteBestimmen","2xIntegrieren"]]));
135 (prep_pbt thy "pbl_bieg_einf" [] e_pblID
136 (["einfache","Biegelinien"],
138 append_rls "e_rls" e_rls [],
140 [["IntegrierenUndKonstanteBestimmen","4x4System"]]));
143 (prep_pbt thy "pbl_bieg_momquer" [] e_pblID
144 (["QuerkraftUndMomentBestimmte","Biegelinien"],
146 append_rls "e_rls" e_rls [],
148 [["IntegrierenUndKonstanteBestimmen","1xIntegrieren"]]));
151 (prep_pbt thy "pbl_bieg_vonq" [] e_pblID
152 (["vonBelastungZu","Biegelinien"],
153 [("#Given" ,["Streckenlast q_q","FunktionsVariable v_v"]),
154 ("#Find" ,["Funktionen funs'''"])],
155 append_rls "e_rls" e_rls [],
157 [["Biegelinien","ausBelastung"]]));
160 (prep_pbt thy "pbl_bieg_randbed" [] e_pblID
161 (["setzeRandbedingungen","Biegelinien"],
162 [("#Given" ,["Funktionen fun_s","Randbedingungen r_b"]),
163 ("#Find" ,["Gleichungen equs'''"])],
164 append_rls "e_rls" e_rls [],
166 [["Biegelinien","setzeRandbedingungenEin"]]));
169 (prep_pbt thy "pbl_equ_fromfun" [] e_pblID
170 (["makeFunctionTo","equation"],
171 [("#Given" ,["functionEq fu_n","substitution su_b"]),
172 ("#Find" ,["equality equ'''"])],
173 append_rls "e_rls" e_rls [],
175 [["Equation","fromFunction"]]));
181 val srls = Rls {id="srls_IntegrierenUnd..",
183 rew_ord = ("termlessI",termlessI),
184 erls = append_rls "erls_in_srls_IntegrierenUnd.." e_rls
185 [(*for asm in NTH_CONS ...*)
186 Calc ("Orderings.ord_class.less",eval_equ "#less_"),
187 (*2nd NTH_CONS pushes n+-1 into asms*)
188 Calc("Groups.plus_class.plus", eval_binop "#add_")
190 srls = Erls, calc = [],
191 rules = [Thm ("NTH_CONS",num_str @{thm NTH_CONS}),
192 Calc("Groups.plus_class.plus", eval_binop "#add_"),
193 Thm ("NTH_NIL",num_str @{thm NTH_NIL}),
194 Calc("Tools.lhs", eval_lhs"eval_lhs_"),
195 Calc("Tools.rhs", eval_rhs"eval_rhs_"),
196 Calc("Atools.argument'_in",
197 eval_argument_in "Atools.argument'_in")
202 Rls {id="srls_IntegrierenUnd..",
204 rew_ord = ("termlessI",termlessI),
205 erls = append_rls "erls_in_srls_IntegrierenUnd.." e_rls
206 [(*for asm in NTH_CONS ...*)
207 Calc ("Orderings.ord_class.less",eval_equ "#less_"),
208 (*2nd NTH_CONS pushes n+-1 into asms*)
209 Calc("Groups.plus_class.plus", eval_binop "#add_")
211 srls = Erls, calc = [],
212 rules = [Thm ("NTH_CONS",num_str @{thm NTH_CONS}),
213 Calc("Groups.plus_class.plus", eval_binop "#add_"),
214 Thm ("NTH_NIL", num_str @{thm NTH_NIL}),
215 Calc("Tools.lhs", eval_lhs "eval_lhs_"),
216 Calc("Atools.filter'_sameFunId",
217 eval_filter_sameFunId "Atools.filter'_sameFunId"),
218 (*WN070514 just for smltest/../biegelinie.sml ...*)
219 Calc("Atools.sameFunId", eval_sameFunId "Atools.sameFunId"),
220 Thm ("filter_Cons", num_str @{thm filter_Cons}),
221 Thm ("filter_Nil", num_str @{thm filter_Nil}),
222 Thm ("if_True", num_str @{thm if_True}),
223 Thm ("if_False", num_str @{thm if_False}),
224 Thm ("hd_thm", num_str @{thm hd_thm})
231 (prep_met thy "met_biege" [] e_metID
232 (["IntegrierenUndKonstanteBestimmen"],
233 [("#Given" ,["Traegerlaenge l_l", "Streckenlast q_q",
234 "FunktionsVariable v_v"]),
235 (*("#Where",["0 < l_l"]), ...wait for < and handling Arbfix*)
236 ("#Find" ,["Biegelinie b_b"]),
237 ("#Relate",["RandbedingungenBiegung r_b",
238 "RandbedingungenMoment r_m"])
240 {rew_ord'="tless_true",
241 rls' = append_rls "erls_IntegrierenUndK.." e_rls
242 [Calc ("Atools.ident",eval_ident "#ident_"),
243 Thm ("not_true",num_str @{thm not_true}),
244 Thm ("not_false",num_str @{thm not_false})],
245 calc = [], srls = srls, prls = Erls,
246 crls = Atools_erls, nrls = Erls},
247 "Script BiegelinieScript " ^
248 "(l_l::real) (q__q::real) (v_v::real) (b_b::real=>real) " ^
249 "(r_b::bool list) (r_m::bool list) = " ^
250 " (let q___q = Take (q_q v_v = q__q); " ^
251 " q___q = ((Rewrite sym_real_minus_eq_cancel True) @@ " ^
252 " (Rewrite Belastung_Querkraft True)) q___q; " ^
253 " (Q__Q:: bool) = " ^
254 " (SubProblem (Biegelinie',[named,integrate,function], " ^
255 " [diff,integration,named]) " ^
256 " [REAL (rhs q___q), REAL v_v, REAL_REAL Q]); " ^
257 " Q__Q = Rewrite Querkraft_Moment True Q__Q; " ^
259 " (SubProblem (Biegelinie',[named,integrate,function], " ^
260 " [diff,integration,named]) " ^
261 " [REAL (rhs Q__Q), REAL v_v, REAL_REAL M_b]); " ^
262 " e__1 = NTH 1 r_m; " ^
263 " (x__1::real) = argument_in (lhs e__1); " ^
264 " (M__1::bool) = (Substitute [v_v = x__1]) M__M; " ^
265 " M__1 = (Substitute [e__1]) M__1 ; " ^
266 " M__2 = Take M__M; " ^
267 (*without this Take 'Substitute [v_v = x__2]' takes _last formula from ctree_*)
268 " e__2 = NTH 2 r_m; " ^
269 " (x__2::real) = argument_in (lhs e__2); " ^
270 " (M__2::bool) = ((Substitute [v_v = x__2]) @@ " ^
271 " (Substitute [e__2])) M__2; " ^
272 " (c_1_2::bool list) = " ^
273 " (SubProblem (Biegelinie',[linear,system],[no_met]) " ^
274 " [BOOL_LIST [M__1, M__2], REAL_LIST [c,c_2]]); " ^
275 " M__M = Take M__M; " ^
276 " M__M = ((Substitute c_1_2) @@ " ^
277 " (Try (Rewrite_Set_Inst [(bdv_1, c),(bdv_2, c_2)]" ^
278 " simplify_System False)) @@ " ^
279 " (Rewrite Moment_Neigung False) @@ " ^
280 " (Rewrite make_fun_explicit False)) M__M; " ^
281 (*----------------------- and the same once more ------------------------*)
282 " (N__N:: bool) = " ^
283 " (SubProblem (Biegelinie',[named,integrate,function], " ^
284 " [diff,integration,named]) " ^
285 " [REAL (rhs M__M), REAL v_v, REAL_REAL y']); " ^
286 " (B__B:: bool) = " ^
287 " (SubProblem (Biegelinie',[named,integrate,function], " ^
288 " [diff,integration,named]) " ^
289 " [REAL (rhs N__N), REAL v_v, REAL_REAL y]); " ^
290 " e__1 = NTH 1 r_b; " ^
291 " (x__1::real) = argument_in (lhs e__1); " ^
292 " (B__1::bool) = (Substitute [v_v = x__1]) B__B; " ^
293 " B__1 = (Substitute [e__1]) B__1 ; " ^
294 " B__2 = Take B__B; " ^
295 " e__2 = NTH 2 r_b; " ^
296 " (x__2::real) = argument_in (lhs e__2); " ^
297 " (B__2::bool) = ((Substitute [v_v = x__2]) @@ " ^
298 " (Substitute [e__2])) B__2; " ^
299 " (c_1_2::bool list) = " ^
300 " (SubProblem (Biegelinie',[linear,system],[no_met]) " ^
301 " [BOOL_LIST [B__1, B__2], REAL_LIST [c,c_2]]); " ^
302 " B__B = Take B__B; " ^
303 " B__B = ((Substitute c_1_2) @@ " ^
304 " (Rewrite_Set_Inst [(bdv, x)] make_ratpoly_in False)) B__B " ^
311 (prep_met thy "met_biege_2" [] e_metID
312 (["IntegrierenUndKonstanteBestimmen2"],
313 [("#Given" ,["Traegerlaenge l_l", "Streckenlast q__q",
314 "FunktionsVariable v_v"]),
315 (*("#Where",["0 < l_l"]), ...wait for < and handling Arbfix*)
316 ("#Find" ,["Biegelinie b_b"]),
317 ("#Relate",["Randbedingungen r_b"])
319 {rew_ord'="tless_true",
320 rls' = append_rls "erls_IntegrierenUndK.." e_rls
321 [Calc ("Atools.ident",eval_ident "#ident_"),
322 Thm ("not_true",num_str @{thm not_true}),
323 Thm ("not_false",num_str @{thm not_false})],
325 srls = append_rls "erls_IntegrierenUndK.." e_rls
326 [Calc("Tools.rhs", eval_rhs"eval_rhs_"),
327 Calc ("Atools.ident",eval_ident "#ident_"),
328 Thm ("last_thmI",num_str @{thm last_thmI}),
329 Thm ("if_True",num_str @{thm if_True}),
330 Thm ("if_False",num_str @{thm if_False})
332 prls = Erls, crls = Atools_erls, nrls = Erls},
333 "Script Biegelinie2Script " ^
334 "(l_l::real) (q__q::real) (v_v::real) (b_b::real=>real) (r_b::bool list) = " ^
336 " (fun_s:: bool list) = " ^
337 " (SubProblem (Biegelinie',[vonBelastungZu,Biegelinien], " ^
338 " [Biegelinien,ausBelastung]) " ^
339 " [REAL q__q, REAL v_v]); " ^
340 " (equ_s::bool list) = " ^
341 " (SubProblem (Biegelinie',[setzeRandbedingungen,Biegelinien]," ^
342 " [Biegelinien,setzeRandbedingungenEin]) " ^
343 " [BOOL_LIST fun_s, BOOL_LIST r_b]); " ^
344 " (con_s::bool list) = " ^
345 " (SubProblem (Biegelinie',[linear,system],[no_met]) " ^
346 " [BOOL_LIST equ_s, REAL_LIST [c,c_2,c_3,c_4]]); " ^
347 " B_B = Take (lastI fun_s); " ^
348 " B_B = ((Substitute con_s) @@ " ^
349 " (Rewrite_Set_Inst [(bdv, v_v)] make_ratpoly_in False)) B_B " ^
356 (prep_met thy "met_biege_intconst_2" [] e_metID
357 (["IntegrierenUndKonstanteBestimmen","2xIntegrieren"],
359 {rew_ord'="tless_true", rls'=Erls, calc = [],
362 crls = Atools_erls, nrls = e_rls},
367 (prep_met thy "met_biege_intconst_4" [] e_metID
368 (["IntegrierenUndKonstanteBestimmen","4x4System"],
370 {rew_ord'="tless_true", rls'=Erls, calc = [],
373 crls = Atools_erls, nrls = e_rls},
378 (prep_met thy "met_biege_intconst_1" [] e_metID
379 (["IntegrierenUndKonstanteBestimmen","1xIntegrieren"],
381 {rew_ord'="tless_true", rls'=Erls, calc = [],
384 crls = Atools_erls, nrls = e_rls},
389 (prep_met thy "met_biege2" [] e_metID
392 {rew_ord'="tless_true", rls'=Erls, calc = [],
395 crls = Atools_erls, nrls = e_rls},
402 (prep_met thy "met_biege_ausbelast" [] e_metID
403 (["Biegelinien","ausBelastung"],
404 [("#Given" ,["Streckenlast q__q","FunktionsVariable v_v"]),
405 ("#Find" ,["Funktionen fun_s"])],
406 {rew_ord'="tless_true",
407 rls' = append_rls "erls_ausBelastung" e_rls
408 [Calc ("Atools.ident",eval_ident "#ident_"),
409 Thm ("not_true",num_str @{thm not_true}),
410 Thm ("not_false",num_str @{thm not_false})],
412 srls = append_rls "srls_ausBelastung" e_rls
413 [Calc("Tools.rhs", eval_rhs"eval_rhs_")],
414 prls = e_rls, crls = Atools_erls, nrls = e_rls},
415 "Script Belastung2BiegelScript (q__q::real) (v_v::real) = " ^
416 " (let q___q = Take (q_q v_v = q__q); " ^
417 " q___q = ((Rewrite sym_real_minus_eq_cancel True) @@ " ^
418 " (Rewrite Belastung_Querkraft True)) q___q; " ^
419 " (Q__Q:: bool) = " ^
420 " (SubProblem (Biegelinie',[named,integrate,function], " ^
421 " [diff,integration,named]) " ^
422 " [REAL (rhs q___q), REAL v_v, REAL_REAL Q]); " ^
423 " M__M = Rewrite Querkraft_Moment True Q__Q; " ^
425 " (SubProblem (Biegelinie',[named,integrate,function], " ^
426 " [diff,integration,named]) " ^
427 " [REAL (rhs M__M), REAL v_v, REAL_REAL M_b]); " ^
428 " N__N = ((Rewrite Moment_Neigung False) @@ " ^
429 " (Rewrite make_fun_explicit False)) M__M; " ^
430 " (N__N:: bool) = " ^
431 " (SubProblem (Biegelinie',[named,integrate,function], " ^
432 " [diff,integration,named]) " ^
433 " [REAL (rhs N__N), REAL v_v, REAL_REAL y']); " ^
434 " (B__B:: bool) = " ^
435 " (SubProblem (Biegelinie',[named,integrate,function], " ^
436 " [diff,integration,named]) " ^
437 " [REAL (rhs N__N), REAL v_v, REAL_REAL y]) " ^
438 " in [Q__Q, M__M, N__N, B__B])"
444 (prep_met thy "met_biege_setzrand" [] e_metID
445 (["Biegelinien","setzeRandbedingungenEin"],
446 [("#Given" ,["Funktionen fun_s","Randbedingungen r_b"]),
447 ("#Find" ,["Gleichungen equs'''"])],
448 {rew_ord'="tless_true", rls'=Erls, calc = [],
451 crls = Atools_erls, nrls = e_rls},
452 "Script SetzeRandbedScript (fun_s::bool list) (r_b::bool list) = " ^
453 " (let b_1 = NTH 1 r_b; " ^
454 " f_s = filter_sameFunId (lhs b_1) fun_s; " ^
456 " (SubProblem (Biegelinie',[makeFunctionTo,equation]," ^
457 " [Equation,fromFunction]) " ^
458 " [BOOL (hd f_s), BOOL b_1]); " ^
459 " b_2 = NTH 2 r_b; " ^
460 " f_s = filter_sameFunId (lhs b_2) fun_s; " ^
462 " (SubProblem (Biegelinie',[makeFunctionTo,equation]," ^
463 " [Equation,fromFunction]) " ^
464 " [BOOL (hd f_s), BOOL b_2]); " ^
465 " b_3 = NTH 3 r_b; " ^
466 " f_s = filter_sameFunId (lhs b_3) fun_s; " ^
468 " (SubProblem (Biegelinie',[makeFunctionTo,equation]," ^
469 " [Equation,fromFunction]) " ^
470 " [BOOL (hd f_s), BOOL b_3]); " ^
471 " b_4 = NTH 4 r_b; " ^
472 " f_s = filter_sameFunId (lhs b_4) fun_s; " ^
474 " (SubProblem (Biegelinie',[makeFunctionTo,equation]," ^
475 " [Equation,fromFunction]) " ^
476 " [BOOL (hd f_s), BOOL b_4]) " ^
477 " in [e_1,e_2,e_3,e_4])"
478 (* filter requires more than 1 sec !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!
479 "Script SetzeRandbedScript (fun_s::bool list) (r_b::bool list) = " ^
480 " (let b_1 = NTH 1 r_b; " ^
481 " f_s = filter (sameFunId (lhs b_1)) fun_s; " ^
483 " (SubProblem (Biegelinie',[makeFunctionTo,equation]," ^
484 " [Equation,fromFunction]) " ^
485 " [BOOL (hd f_s), BOOL b_1]); " ^
486 " b_2 = NTH 2 r_b; " ^
487 " f_s = filter (sameFunId (lhs b_2)) fun_s; " ^
489 " (SubProblem (Biegelinie',[makeFunctionTo,equation]," ^
490 " [Equation,fromFunction]) " ^
491 " [BOOL (hd f_s), BOOL b_2]); " ^
492 " b_3 = NTH 3 r_b; " ^
493 " f_s = filter (sameFunId (lhs b_3)) fun_s; " ^
495 " (SubProblem (Biegelinie',[makeFunctionTo,equation]," ^
496 " [Equation,fromFunction]) " ^
497 " [BOOL (hd f_s), BOOL b_3]); " ^
498 " b_4 = NTH 4 r_b; " ^
499 " f_s = filter (sameFunId (lhs b_4)) fun_s; " ^
501 " (SubProblem (Biegelinie',[makeFunctionTo,equation]," ^
502 " [Equation,fromFunction]) " ^
503 " [BOOL (hd f_s), BOOL b_4]) " ^
504 " in [e_1,e_2,e_3,e_4])"*)
510 (prep_met thy "met_equ_fromfun" [] e_metID
511 (["Equation","fromFunction"],
512 [("#Given" ,["functionEq fu_n","substitution su_b"]),
513 ("#Find" ,["equality equ'''"])],
514 {rew_ord'="tless_true", rls'=Erls, calc = [],
515 srls = append_rls "srls_in_EquationfromFunc" e_rls
516 [Calc("Tools.lhs", eval_lhs"eval_lhs_"),
517 Calc("Atools.argument'_in",
519 "Atools.argument'_in")],
520 prls=e_rls, crls = Atools_erls, nrls = e_rls},
521 (*(M_b x = c_2 + c * x + -1 * q_0 / 2 * x ^^^ 2) (M_b L = 0) -->
522 0 = c_2 + c * L + -1 * q_0 / 2 * L ^^^ 2*)
523 "Script Function2Equality (fu_n::bool) (su_b::bool) =" ^
524 " (let fu_n = Take fu_n; " ^
525 " bd_v = argument_in (lhs fu_n); " ^
526 " va_l = argument_in (lhs su_b); " ^
527 " eq_u = (Substitute [bd_v = va_l]) fu_n; " ^
528 " eq_u = (Substitute [su_b]) fu_n " ^
529 " in (Rewrite_Set norm_Rational False) eq_u) "