132 ("#Where" ,["False", (*WN0509 just detected: this pbl can never be used?!?*) |
132 ("#Where" ,["False", (*WN0509 just detected: this pbl can never be used?!?*) |
133 "Not( (lhs e_e) is_polyrat_in v_v)", |
133 "Not( (lhs e_e) is_polyrat_in v_v)", |
134 "Not( (rhs e_e) is_polyrat_in v_v)", |
134 "Not( (rhs e_e) is_polyrat_in v_v)", |
135 "((lhs e_e) has_degree_in v_v)=1", |
135 "((lhs e_e) has_degree_in v_v)=1", |
136 "((rhs e_e) has_degree_in v_v)=1"]), |
136 "((rhs e_e) has_degree_in v_v)=1"]), |
137 ("#Find" ,["solutions v'i'"]) |
137 ("#Find" ,["solutions v_v'i'"]) |
138 ], |
138 ], |
139 LinEq_prls, SOME "solve (e_e::bool, v_v)", |
139 LinEq_prls, SOME "solve (e_e::bool, v_v)", |
140 [["LinEq","solve_lineq_equation"]])); |
140 [["LinEq","solve_lineq_equation"]])); |
141 |
141 |
142 (*-------------- methods------------------------------------------------------*) |
142 (*-------------- methods------------------------------------------------------*) |
153 (prep_met thy "met_eq_lin" [] e_metID |
153 (prep_met thy "met_eq_lin" [] e_metID |
154 (["LinEq","solve_lineq_equation"], |
154 (["LinEq","solve_lineq_equation"], |
155 [("#Given", ["equality e_e", "solveFor v_v"]), |
155 [("#Given", ["equality e_e", "solveFor v_v"]), |
156 ("#Where", ["Not ((lhs e_e) is_polyrat_in v_v)", |
156 ("#Where", ["Not ((lhs e_e) is_polyrat_in v_v)", |
157 "((lhs e_e) has_degree_in v_v) = 1"]), |
157 "((lhs e_e) has_degree_in v_v) = 1"]), |
158 ("#Find", ["solutions v'i'"]) |
158 ("#Find", ["solutions v_v'i'"]) |
159 ], |
159 ], |
160 {rew_ord'="termlessI", rls'=LinEq_erls, srls=e_rls, prls=LinEq_prls, |
160 {rew_ord'="termlessI", rls'=LinEq_erls, srls=e_rls, prls=LinEq_prls, |
161 calc=[], crls=LinEq_crls, nrls=norm_Poly}, |
161 calc=[], crls=LinEq_crls, nrls=norm_Poly}, |
162 "Script Solve_lineq_equation (e_e::bool) (v_v::real) = " ^ |
162 "Script Solve_lineq_equation (e_e::bool) (v_v::real) = " ^ |
163 "(let e_e =((Try (Rewrite all_left False)) @@ " ^ |
163 "(let e_e =((Try (Rewrite all_left False)) @@ " ^ |