142 (prep_pbt thy "pbl_equ_univ_root_sq_rat" [] e_pblID |
142 (prep_pbt thy "pbl_equ_univ_root_sq_rat" [] e_pblID |
143 (["rat","sq","root'","univariate","equation"], |
143 (["rat","sq","root'","univariate","equation"], |
144 [("#Given" ,["equality e_e","solveFor v_v"]), |
144 [("#Given" ,["equality e_e","solveFor v_v"]), |
145 ("#Where" ,["( (lhs e_e) is_rootRatAddTerm_in (v_v::real) )| " ^ |
145 ("#Where" ,["( (lhs e_e) is_rootRatAddTerm_in (v_v::real) )| " ^ |
146 "( (rhs e_e) is_rootRatAddTerm_in (v_v::real) )"]), |
146 "( (rhs e_e) is_rootRatAddTerm_in (v_v::real) )"]), |
147 ("#Find" ,["solutions v_i"]) |
147 ("#Find" ,["solutions v_i'''"]) |
148 ], |
148 ], |
149 RootRatEq_prls, SOME "solve (e_e::bool, v_v)", |
149 RootRatEq_prls, SOME "solve (e_e::bool, v_v)", |
150 [["RootRatEq","elim_rootrat_equation"]])); |
150 [["RootRatEq","elim_rootrat_equation"]])); |
151 *} |
151 *} |
152 ML {* |
152 ML {* |
162 (prep_met thy "met_rootrateq_elim" [] e_metID |
162 (prep_met thy "met_rootrateq_elim" [] e_metID |
163 (["RootRatEq","elim_rootrat_equation"], |
163 (["RootRatEq","elim_rootrat_equation"], |
164 [("#Given" ,["equality e_e","solveFor v_v"]), |
164 [("#Given" ,["equality e_e","solveFor v_v"]), |
165 ("#Where" ,["( (lhs e_e) is_rootRatAddTerm_in (v_v::real) ) | " ^ |
165 ("#Where" ,["( (lhs e_e) is_rootRatAddTerm_in (v_v::real) ) | " ^ |
166 "( (rhs e_e) is_rootRatAddTerm_in (v_v::real) )"]), |
166 "( (rhs e_e) is_rootRatAddTerm_in (v_v::real) )"]), |
167 ("#Find" ,["solutions v_i"]) |
167 ("#Find" ,["solutions v_i'''"]) |
168 ], |
168 ], |
169 {rew_ord'="termlessI", |
169 {rew_ord'="termlessI", |
170 rls'=RooRatEq_erls, |
170 rls'=RooRatEq_erls, |
171 srls=e_rls, |
171 srls=e_rls, |
172 prls=RootRatEq_prls, |
172 prls=RootRatEq_prls, |