1 (*.(c) by Richard Lang, 2003 .*) |
|
2 (* theory collecting all knowledge |
|
3 (predicates 'is_rootEq_in', 'is_sqrt_in', 'is_ratEq_in') |
|
4 for PolynomialEquations. |
|
5 alternative dependencies see Isac.thy |
|
6 created by: rlang |
|
7 date: 02.07 |
|
8 changed by: rlang |
|
9 last change by: rlang |
|
10 date: 03.06.03 |
|
11 *) |
|
12 |
|
13 (* remove_thy"PolyEq"; |
|
14 use_thy"IsacKnowledge/Isac"; |
|
15 use_thy"IsacKnowledge/PolyEq"; |
|
16 |
|
17 remove_thy"PolyEq"; |
|
18 use_thy"Isac"; |
|
19 |
|
20 use"ROOT.ML"; |
|
21 cd"knowledge"; |
|
22 *) |
|
23 |
|
24 PolyEq = LinEq + RootRatEq + |
|
25 (*-------------------- consts ------------------------------------------------*) |
|
26 consts |
|
27 |
|
28 (*---------scripts--------------------------*) |
|
29 Complete'_square |
|
30 :: "[bool,real, \ |
|
31 \ bool list] => bool list" |
|
32 ("((Script Complete'_square (_ _ =))// \ |
|
33 \ (_))" 9) |
|
34 (*----- poly ----- *) |
|
35 Normalize'_poly |
|
36 :: "[bool,real, \ |
|
37 \ bool list] => bool list" |
|
38 ("((Script Normalize'_poly (_ _=))// \ |
|
39 \ (_))" 9) |
|
40 Solve'_d0'_polyeq'_equation |
|
41 :: "[bool,real, \ |
|
42 \ bool list] => bool list" |
|
43 ("((Script Solve'_d0'_polyeq'_equation (_ _ =))// \ |
|
44 \ (_))" 9) |
|
45 Solve'_d1'_polyeq'_equation |
|
46 :: "[bool,real, \ |
|
47 \ bool list] => bool list" |
|
48 ("((Script Solve'_d1'_polyeq'_equation (_ _ =))// \ |
|
49 \ (_))" 9) |
|
50 Solve'_d2'_polyeq'_equation |
|
51 :: "[bool,real, \ |
|
52 \ bool list] => bool list" |
|
53 ("((Script Solve'_d2'_polyeq'_equation (_ _ =))// \ |
|
54 \ (_))" 9) |
|
55 Solve'_d2'_polyeq'_sqonly'_equation |
|
56 :: "[bool,real, \ |
|
57 \ bool list] => bool list" |
|
58 ("((Script Solve'_d2'_polyeq'_sqonly'_equation (_ _ =))// \ |
|
59 \ (_))" 9) |
|
60 Solve'_d2'_polyeq'_bdvonly'_equation |
|
61 :: "[bool,real, \ |
|
62 \ bool list] => bool list" |
|
63 ("((Script Solve'_d2'_polyeq'_bdvonly'_equation (_ _ =))// \ |
|
64 \ (_))" 9) |
|
65 Solve'_d2'_polyeq'_pq'_equation |
|
66 :: "[bool,real, \ |
|
67 \ bool list] => bool list" |
|
68 ("((Script Solve'_d2'_polyeq'_pq'_equation (_ _ =))// \ |
|
69 \ (_))" 9) |
|
70 Solve'_d2'_polyeq'_abc'_equation |
|
71 :: "[bool,real, \ |
|
72 \ bool list] => bool list" |
|
73 ("((Script Solve'_d2'_polyeq'_abc'_equation (_ _ =))// \ |
|
74 \ (_))" 9) |
|
75 Solve'_d3'_polyeq'_equation |
|
76 :: "[bool,real, \ |
|
77 \ bool list] => bool list" |
|
78 ("((Script Solve'_d3'_polyeq'_equation (_ _ =))// \ |
|
79 \ (_))" 9) |
|
80 Solve'_d4'_polyeq'_equation |
|
81 :: "[bool,real, \ |
|
82 \ bool list] => bool list" |
|
83 ("((Script Solve'_d4'_polyeq'_equation (_ _ =))// \ |
|
84 \ (_))" 9) |
|
85 Biquadrat'_poly |
|
86 :: "[bool,real, \ |
|
87 \ bool list] => bool list" |
|
88 ("((Script Biquadrat'_poly (_ _=))// \ |
|
89 \ (_))" 9) |
|
90 |
|
91 (*-------------------- rules -------------------------------------------------*) |
|
92 rules |
|
93 |
|
94 cancel_leading_coeff1 "Not (c =!= 0) ==> (a + b*bdv + c*bdv^^^2 = 0) = \ |
|
95 \ (a/c + b/c*bdv + bdv^^^2 = 0)" |
|
96 cancel_leading_coeff2 "Not (c =!= 0) ==> (a - b*bdv + c*bdv^^^2 = 0) = \ |
|
97 \ (a/c - b/c*bdv + bdv^^^2 = 0)" |
|
98 cancel_leading_coeff3 "Not (c =!= 0) ==> (a + b*bdv - c*bdv^^^2 = 0) = \ |
|
99 \ (a/c + b/c*bdv - bdv^^^2 = 0)" |
|
100 |
|
101 cancel_leading_coeff4 "Not (c =!= 0) ==> (a + bdv + c*bdv^^^2 = 0) = \ |
|
102 \ (a/c + 1/c*bdv + bdv^^^2 = 0)" |
|
103 cancel_leading_coeff5 "Not (c =!= 0) ==> (a - bdv + c*bdv^^^2 = 0) = \ |
|
104 \ (a/c - 1/c*bdv + bdv^^^2 = 0)" |
|
105 cancel_leading_coeff6 "Not (c =!= 0) ==> (a + bdv - c*bdv^^^2 = 0) = \ |
|
106 \ (a/c + 1/c*bdv - bdv^^^2 = 0)" |
|
107 |
|
108 cancel_leading_coeff7 "Not (c =!= 0) ==> ( b*bdv + c*bdv^^^2 = 0) = \ |
|
109 \ ( b/c*bdv + bdv^^^2 = 0)" |
|
110 cancel_leading_coeff8 "Not (c =!= 0) ==> ( b*bdv - c*bdv^^^2 = 0) = \ |
|
111 \ ( b/c*bdv - bdv^^^2 = 0)" |
|
112 |
|
113 cancel_leading_coeff9 "Not (c =!= 0) ==> ( bdv + c*bdv^^^2 = 0) = \ |
|
114 \ ( 1/c*bdv + bdv^^^2 = 0)" |
|
115 cancel_leading_coeff10"Not (c =!= 0) ==> ( bdv - c*bdv^^^2 = 0) = \ |
|
116 \ ( 1/c*bdv - bdv^^^2 = 0)" |
|
117 |
|
118 cancel_leading_coeff11"Not (c =!= 0) ==> (a + b*bdv^^^2 = 0) = \ |
|
119 \ (a/b + bdv^^^2 = 0)" |
|
120 cancel_leading_coeff12"Not (c =!= 0) ==> (a - b*bdv^^^2 = 0) = \ |
|
121 \ (a/b - bdv^^^2 = 0)" |
|
122 cancel_leading_coeff13"Not (c =!= 0) ==> ( b*bdv^^^2 = 0) = \ |
|
123 \ ( bdv^^^2 = 0/b)" |
|
124 |
|
125 complete_square1 "(q + p*bdv + bdv^^^2 = 0) = \ |
|
126 \(q + (p/2 + bdv)^^^2 = (p/2)^^^2)" |
|
127 complete_square2 "( p*bdv + bdv^^^2 = 0) = \ |
|
128 \( (p/2 + bdv)^^^2 = (p/2)^^^2)" |
|
129 complete_square3 "( bdv + bdv^^^2 = 0) = \ |
|
130 \( (1/2 + bdv)^^^2 = (1/2)^^^2)" |
|
131 |
|
132 complete_square4 "(q - p*bdv + bdv^^^2 = 0) = \ |
|
133 \(q + (p/2 - bdv)^^^2 = (p/2)^^^2)" |
|
134 complete_square5 "(q + p*bdv - bdv^^^2 = 0) = \ |
|
135 \(q + (p/2 - bdv)^^^2 = (p/2)^^^2)" |
|
136 |
|
137 square_explicit1 "(a + b^^^2 = c) = ( b^^^2 = c - a)" |
|
138 square_explicit2 "(a - b^^^2 = c) = (-(b^^^2) = c - a)" |
|
139 |
|
140 bdv_explicit1 "(a + bdv = b) = (bdv = - a + b)" |
|
141 bdv_explicit2 "(a - bdv = b) = ((-1)*bdv = - a + b)" |
|
142 bdv_explicit3 "((-1)*bdv = b) = (bdv = (-1)*b)" |
|
143 |
|
144 plus_leq "(0 <= a + b) = ((-1)*b <= a)"(*Isa?*) |
|
145 minus_leq "(0 <= a - b) = ( b <= a)"(*Isa?*) |
|
146 |
|
147 (*-- normalize --*) |
|
148 (*WN0509 compare LinEq.all_left "[|Not(b=!=0)|] ==> (a=b) = (a+(-1)*b=0)"*) |
|
149 all_left |
|
150 "[|Not(b=!=0)|] ==> (a = b) = (a - b = 0)" |
|
151 makex1_x |
|
152 "a^^^1 = a" |
|
153 real_assoc_1 |
|
154 "a+(b+c) = a+b+c" |
|
155 real_assoc_2 |
|
156 "a*(b*c) = a*b*c" |
|
157 |
|
158 (* ---- degree 0 ----*) |
|
159 d0_true |
|
160 "(0=0) = True" |
|
161 d0_false |
|
162 "[|Not(bdv occurs_in a);Not(a=0)|] ==> (a=0) = False" |
|
163 (* ---- degree 1 ----*) |
|
164 d1_isolate_add1 |
|
165 "[|Not(bdv occurs_in a)|] ==> (a + b*bdv = 0) = (b*bdv = (-1)*a)" |
|
166 d1_isolate_add2 |
|
167 "[|Not(bdv occurs_in a)|] ==> (a + bdv = 0) = ( bdv = (-1)*a)" |
|
168 d1_isolate_div |
|
169 "[|Not(b=0);Not(bdv occurs_in c)|] ==> (b*bdv = c) = (bdv = c/b)" |
|
170 (* ---- degree 2 ----*) |
|
171 d2_isolate_add1 |
|
172 "[|Not(bdv occurs_in a)|] ==> (a + b*bdv^^^2=0) = (b*bdv^^^2= (-1)*a)" |
|
173 d2_isolate_add2 |
|
174 "[|Not(bdv occurs_in a)|] ==> (a + bdv^^^2=0) = ( bdv^^^2= (-1)*a)" |
|
175 d2_isolate_div |
|
176 "[|Not(b=0);Not(bdv occurs_in c)|] ==> (b*bdv^^^2=c) = (bdv^^^2=c/b)" |
|
177 d2_prescind1 |
|
178 "(a*bdv + b*bdv^^^2 = 0) = (bdv*(a +b*bdv)=0)" |
|
179 d2_prescind2 |
|
180 "(a*bdv + bdv^^^2 = 0) = (bdv*(a + bdv)=0)" |
|
181 d2_prescind3 |
|
182 "( bdv + b*bdv^^^2 = 0) = (bdv*(1+b*bdv)=0)" |
|
183 d2_prescind4 |
|
184 "( bdv + bdv^^^2 = 0) = (bdv*(1+ bdv)=0)" |
|
185 (* eliminate degree 2 *) |
|
186 (* thm for neg arguments in sqroot have postfix _neg *) |
|
187 d2_sqrt_equation1 |
|
188 "[|(0<=c);Not(bdv occurs_in c)|] ==> (bdv^^^2=c) = ((bdv=sqrt c) | (bdv=(-1)*sqrt c ))" |
|
189 d2_sqrt_equation1_neg |
|
190 "[|(c<0);Not(bdv occurs_in c)|] ==> (bdv^^^2=c) = False" |
|
191 d2_sqrt_equation2 |
|
192 "(bdv^^^2=0) = (bdv=0)" |
|
193 d2_sqrt_equation3 |
|
194 "(b*bdv^^^2=0) = (bdv=0)" |
|
195 d2_reduce_equation1 |
|
196 "(bdv*(a +b*bdv)=0) = ((bdv=0)|(a+b*bdv=0))" |
|
197 d2_reduce_equation2 |
|
198 "(bdv*(a + bdv)=0) = ((bdv=0)|(a+ bdv=0))" |
|
199 d2_pqformula1 |
|
200 "[|0<=p^^^2 - 4*q|] ==> (q+p*bdv+ bdv^^^2=0) = |
|
201 ((bdv= (-1)*(p/2) + sqrt(p^^^2 - 4*q)/2) |
|
202 | (bdv= (-1)*(p/2) - sqrt(p^^^2 - 4*q)/2))" |
|
203 d2_pqformula1_neg |
|
204 "[|p^^^2 - 4*q<0|] ==> (q+p*bdv+ bdv^^^2=0) = False" |
|
205 d2_pqformula2 |
|
206 "[|0<=p^^^2 - 4*q|] ==> (q+p*bdv+1*bdv^^^2=0) = |
|
207 ((bdv= (-1)*(p/2) + sqrt(p^^^2 - 4*q)/2) |
|
208 | (bdv= (-1)*(p/2) - sqrt(p^^^2 - 4*q)/2))" |
|
209 d2_pqformula2_neg |
|
210 "[|p^^^2 - 4*q<0|] ==> (q+p*bdv+1*bdv^^^2=0) = False" |
|
211 d2_pqformula3 |
|
212 "[|0<=1 - 4*q|] ==> (q+ bdv+ bdv^^^2=0) = |
|
213 ((bdv= (-1)*(1/2) + sqrt(1 - 4*q)/2) |
|
214 | (bdv= (-1)*(1/2) - sqrt(1 - 4*q)/2))" |
|
215 d2_pqformula3_neg |
|
216 "[|1 - 4*q<0|] ==> (q+ bdv+ bdv^^^2=0) = False" |
|
217 d2_pqformula4 |
|
218 "[|0<=1 - 4*q|] ==> (q+ bdv+1*bdv^^^2=0) = |
|
219 ((bdv= (-1)*(1/2) + sqrt(1 - 4*q)/2) |
|
220 | (bdv= (-1)*(1/2) - sqrt(1 - 4*q)/2))" |
|
221 d2_pqformula4_neg |
|
222 "[|1 - 4*q<0|] ==> (q+ bdv+1*bdv^^^2=0) = False" |
|
223 d2_pqformula5 |
|
224 "[|0<=p^^^2 - 0|] ==> ( p*bdv+ bdv^^^2=0) = |
|
225 ((bdv= (-1)*(p/2) + sqrt(p^^^2 - 0)/2) |
|
226 | (bdv= (-1)*(p/2) - sqrt(p^^^2 - 0)/2))" |
|
227 (* d2_pqformula5_neg not need p^2 never less zero in R *) |
|
228 d2_pqformula6 |
|
229 "[|0<=p^^^2 - 0|] ==> ( p*bdv+1*bdv^^^2=0) = |
|
230 ((bdv= (-1)*(p/2) + sqrt(p^^^2 - 0)/2) |
|
231 | (bdv= (-1)*(p/2) - sqrt(p^^^2 - 0)/2))" |
|
232 (* d2_pqformula6_neg not need p^2 never less zero in R *) |
|
233 d2_pqformula7 |
|
234 "[|0<=1 - 0|] ==> ( bdv+ bdv^^^2=0) = |
|
235 ((bdv= (-1)*(1/2) + sqrt(1 - 0)/2) |
|
236 | (bdv= (-1)*(1/2) - sqrt(1 - 0)/2))" |
|
237 (* d2_pqformula7_neg not need, because 1<0 ==> False*) |
|
238 d2_pqformula8 |
|
239 "[|0<=1 - 0|] ==> ( bdv+1*bdv^^^2=0) = |
|
240 ((bdv= (-1)*(1/2) + sqrt(1 - 0)/2) |
|
241 | (bdv= (-1)*(1/2) - sqrt(1 - 0)/2))" |
|
242 (* d2_pqformula8_neg not need, because 1<0 ==> False*) |
|
243 d2_pqformula9 |
|
244 "[|Not(bdv occurs_in q); 0<= (-1)*4*q|] ==> (q+ 1*bdv^^^2=0) = |
|
245 ((bdv= 0 + sqrt(0 - 4*q)/2) |
|
246 | (bdv= 0 - sqrt(0 - 4*q)/2))" |
|
247 d2_pqformula9_neg |
|
248 "[|Not(bdv occurs_in q); (-1)*4*q<0|] ==> (q+ 1*bdv^^^2=0) = False" |
|
249 d2_pqformula10 |
|
250 "[|Not(bdv occurs_in q); 0<= (-1)*4*q|] ==> (q+ bdv^^^2=0) = |
|
251 ((bdv= 0 + sqrt(0 - 4*q)/2) |
|
252 | (bdv= 0 - sqrt(0 - 4*q)/2))" |
|
253 d2_pqformula10_neg |
|
254 "[|Not(bdv occurs_in q); (-1)*4*q<0|] ==> (q+ bdv^^^2=0) = False" |
|
255 d2_abcformula1 |
|
256 "[|0<=b^^^2 - 4*a*c|] ==> (c + b*bdv+a*bdv^^^2=0) = |
|
257 ((bdv=( -b + sqrt(b^^^2 - 4*a*c))/(2*a)) |
|
258 | (bdv=( -b - sqrt(b^^^2 - 4*a*c))/(2*a)))" |
|
259 d2_abcformula1_neg |
|
260 "[|b^^^2 - 4*a*c<0|] ==> (c + b*bdv+a*bdv^^^2=0) = False" |
|
261 d2_abcformula2 |
|
262 "[|0<=1 - 4*a*c|] ==> (c+ bdv+a*bdv^^^2=0) = |
|
263 ((bdv=( -1 + sqrt(1 - 4*a*c))/(2*a)) |
|
264 | (bdv=( -1 - sqrt(1 - 4*a*c))/(2*a)))" |
|
265 d2_abcformula2_neg |
|
266 "[|1 - 4*a*c<0|] ==> (c+ bdv+a*bdv^^^2=0) = False" |
|
267 d2_abcformula3 |
|
268 "[|0<=b^^^2 - 4*1*c|] ==> (c + b*bdv+ bdv^^^2=0) = |
|
269 ((bdv=( -b + sqrt(b^^^2 - 4*1*c))/(2*1)) |
|
270 | (bdv=( -b - sqrt(b^^^2 - 4*1*c))/(2*1)))" |
|
271 d2_abcformula3_neg |
|
272 "[|b^^^2 - 4*1*c<0|] ==> (c + b*bdv+ bdv^^^2=0) = False" |
|
273 d2_abcformula4 |
|
274 "[|0<=1 - 4*1*c|] ==> (c + bdv+ bdv^^^2=0) = |
|
275 ((bdv=( -1 + sqrt(1 - 4*1*c))/(2*1)) |
|
276 | (bdv=( -1 - sqrt(1 - 4*1*c))/(2*1)))" |
|
277 d2_abcformula4_neg |
|
278 "[|1 - 4*1*c<0|] ==> (c + bdv+ bdv^^^2=0) = False" |
|
279 d2_abcformula5 |
|
280 "[|Not(bdv occurs_in c); 0<=0 - 4*a*c|] ==> (c + a*bdv^^^2=0) = |
|
281 ((bdv=( 0 + sqrt(0 - 4*a*c))/(2*a)) |
|
282 | (bdv=( 0 - sqrt(0 - 4*a*c))/(2*a)))" |
|
283 d2_abcformula5_neg |
|
284 "[|Not(bdv occurs_in c); 0 - 4*a*c<0|] ==> (c + a*bdv^^^2=0) = False" |
|
285 d2_abcformula6 |
|
286 "[|Not(bdv occurs_in c); 0<=0 - 4*1*c|] ==> (c+ bdv^^^2=0) = |
|
287 ((bdv=( 0 + sqrt(0 - 4*1*c))/(2*1)) |
|
288 | (bdv=( 0 - sqrt(0 - 4*1*c))/(2*1)))" |
|
289 d2_abcformula6_neg |
|
290 "[|Not(bdv occurs_in c); 0 - 4*1*c<0|] ==> (c+ bdv^^^2=0) = False" |
|
291 d2_abcformula7 |
|
292 "[|0<=b^^^2 - 0|] ==> ( b*bdv+a*bdv^^^2=0) = |
|
293 ((bdv=( -b + sqrt(b^^^2 - 0))/(2*a)) |
|
294 | (bdv=( -b - sqrt(b^^^2 - 0))/(2*a)))" |
|
295 (* d2_abcformula7_neg not need b^2 never less zero in R *) |
|
296 d2_abcformula8 |
|
297 "[|0<=b^^^2 - 0|] ==> ( b*bdv+ bdv^^^2=0) = |
|
298 ((bdv=( -b + sqrt(b^^^2 - 0))/(2*1)) |
|
299 | (bdv=( -b - sqrt(b^^^2 - 0))/(2*1)))" |
|
300 (* d2_abcformula8_neg not need b^2 never less zero in R *) |
|
301 d2_abcformula9 |
|
302 "[|0<=1 - 0|] ==> ( bdv+a*bdv^^^2=0) = |
|
303 ((bdv=( -1 + sqrt(1 - 0))/(2*a)) |
|
304 | (bdv=( -1 - sqrt(1 - 0))/(2*a)))" |
|
305 (* d2_abcformula9_neg not need, because 1<0 ==> False*) |
|
306 d2_abcformula10 |
|
307 "[|0<=1 - 0|] ==> ( bdv+ bdv^^^2=0) = |
|
308 ((bdv=( -1 + sqrt(1 - 0))/(2*1)) |
|
309 | (bdv=( -1 - sqrt(1 - 0))/(2*1)))" |
|
310 (* d2_abcformula10_neg not need, because 1<0 ==> False*) |
|
311 |
|
312 (* ---- degree 3 ----*) |
|
313 d3_reduce_equation1 |
|
314 "(a*bdv + b*bdv^^^2 + c*bdv^^^3=0) = (bdv=0 | (a + b*bdv + c*bdv^^^2=0))" |
|
315 d3_reduce_equation2 |
|
316 "( bdv + b*bdv^^^2 + c*bdv^^^3=0) = (bdv=0 | (1 + b*bdv + c*bdv^^^2=0))" |
|
317 d3_reduce_equation3 |
|
318 "(a*bdv + bdv^^^2 + c*bdv^^^3=0) = (bdv=0 | (a + bdv + c*bdv^^^2=0))" |
|
319 d3_reduce_equation4 |
|
320 "( bdv + bdv^^^2 + c*bdv^^^3=0) = (bdv=0 | (1 + bdv + c*bdv^^^2=0))" |
|
321 d3_reduce_equation5 |
|
322 "(a*bdv + b*bdv^^^2 + bdv^^^3=0) = (bdv=0 | (a + b*bdv + bdv^^^2=0))" |
|
323 d3_reduce_equation6 |
|
324 "( bdv + b*bdv^^^2 + bdv^^^3=0) = (bdv=0 | (1 + b*bdv + bdv^^^2=0))" |
|
325 d3_reduce_equation7 |
|
326 "(a*bdv + bdv^^^2 + bdv^^^3=0) = (bdv=0 | (1 + bdv + bdv^^^2=0))" |
|
327 d3_reduce_equation8 |
|
328 "( bdv + bdv^^^2 + bdv^^^3=0) = (bdv=0 | (1 + bdv + bdv^^^2=0))" |
|
329 d3_reduce_equation9 |
|
330 "(a*bdv + c*bdv^^^3=0) = (bdv=0 | (a + c*bdv^^^2=0))" |
|
331 d3_reduce_equation10 |
|
332 "( bdv + c*bdv^^^3=0) = (bdv=0 | (1 + c*bdv^^^2=0))" |
|
333 d3_reduce_equation11 |
|
334 "(a*bdv + bdv^^^3=0) = (bdv=0 | (a + bdv^^^2=0))" |
|
335 d3_reduce_equation12 |
|
336 "( bdv + bdv^^^3=0) = (bdv=0 | (1 + bdv^^^2=0))" |
|
337 d3_reduce_equation13 |
|
338 "( b*bdv^^^2 + c*bdv^^^3=0) = (bdv=0 | ( b*bdv + c*bdv^^^2=0))" |
|
339 d3_reduce_equation14 |
|
340 "( bdv^^^2 + c*bdv^^^3=0) = (bdv=0 | ( bdv + c*bdv^^^2=0))" |
|
341 d3_reduce_equation15 |
|
342 "( b*bdv^^^2 + bdv^^^3=0) = (bdv=0 | ( b*bdv + bdv^^^2=0))" |
|
343 d3_reduce_equation16 |
|
344 "( bdv^^^2 + bdv^^^3=0) = (bdv=0 | ( bdv + bdv^^^2=0))" |
|
345 d3_isolate_add1 |
|
346 "[|Not(bdv occurs_in a)|] ==> (a + b*bdv^^^3=0) = (b*bdv^^^3= (-1)*a)" |
|
347 d3_isolate_add2 |
|
348 "[|Not(bdv occurs_in a)|] ==> (a + bdv^^^3=0) = ( bdv^^^3= (-1)*a)" |
|
349 d3_isolate_div |
|
350 "[|Not(b=0);Not(bdv occurs_in a)|] ==> (b*bdv^^^3=c) = (bdv^^^3=c/b)" |
|
351 d3_root_equation2 |
|
352 "(bdv^^^3=0) = (bdv=0)" |
|
353 d3_root_equation1 |
|
354 "(bdv^^^3=c) = (bdv = nroot 3 c)" |
|
355 |
|
356 (* ---- degree 4 ----*) |
|
357 (* RL03.FIXME es wir nicht getestet ob u>0 *) |
|
358 d4_sub_u1 |
|
359 "(c+b*bdv^^^2+a*bdv^^^4=0) = |
|
360 ((a*u^^^2+b*u+c=0) & (bdv^^^2=u))" |
|
361 |
|
362 (* ---- 7.3.02 von Termorder ---- *) |
|
363 |
|
364 bdv_collect_1 "l * bdv + m * bdv = (l + m) * bdv" |
|
365 bdv_collect_2 "bdv + m * bdv = (1 + m) * bdv" |
|
366 bdv_collect_3 "l * bdv + bdv = (l + 1) * bdv" |
|
367 |
|
368 (* bdv_collect_assoc0_1 "l * bdv + m * bdv + k = (l + m) * bdv + k" |
|
369 bdv_collect_assoc0_2 "bdv + m * bdv + k = (1 + m) * bdv + k" |
|
370 bdv_collect_assoc0_3 "l * bdv + bdv + k = (l + 1) * bdv + k" |
|
371 *) |
|
372 bdv_collect_assoc1_1 "l * bdv + (m * bdv + k) = (l + m) * bdv + k" |
|
373 bdv_collect_assoc1_2 "bdv + (m * bdv + k) = (1 + m) * bdv + k" |
|
374 bdv_collect_assoc1_3 "l * bdv + (bdv + k) = (l + 1) * bdv + k" |
|
375 |
|
376 bdv_collect_assoc2_1 "k + l * bdv + m * bdv = k + (l + m) * bdv" |
|
377 bdv_collect_assoc2_2 "k + bdv + m * bdv = k + (1 + m) * bdv" |
|
378 bdv_collect_assoc2_3 "k + l * bdv + bdv = k + (l + 1) * bdv" |
|
379 |
|
380 |
|
381 bdv_n_collect_1 "l * bdv^^^n + m * bdv^^^n = (l + m) * bdv^^^n" |
|
382 bdv_n_collect_2 " bdv^^^n + m * bdv^^^n = (1 + m) * bdv^^^n" |
|
383 bdv_n_collect_3 "l * bdv^^^n + bdv^^^n = (l + 1) * bdv^^^n" (*order!*) |
|
384 |
|
385 bdv_n_collect_assoc1_1 "l * bdv^^^n + (m * bdv^^^n + k) = (l + m) * bdv^^^n + k" |
|
386 bdv_n_collect_assoc1_2 "bdv^^^n + (m * bdv^^^n + k) = (1 + m) * bdv^^^n + k" |
|
387 bdv_n_collect_assoc1_3 "l * bdv^^^n + (bdv^^^n + k) = (l + 1) * bdv^^^n + k" |
|
388 |
|
389 bdv_n_collect_assoc2_1 "k + l * bdv^^^n + m * bdv^^^n = k + (l + m) * bdv^^^n" |
|
390 bdv_n_collect_assoc2_2 "k + bdv^^^n + m * bdv^^^n = k + (1 + m) * bdv^^^n" |
|
391 bdv_n_collect_assoc2_3 "k + l * bdv^^^n + bdv^^^n = k + (l + 1) * bdv^^^n" |
|
392 |
|
393 (*WN.14.3.03*) |
|
394 real_minus_div "- (a / b) = (-1 * a) / b" |
|
395 |
|
396 separate_bdv "(a * bdv) / b = (a / b) * bdv" |
|
397 separate_bdv_n "(a * bdv ^^^ n) / b = (a / b) * bdv ^^^ n" |
|
398 separate_1_bdv "bdv / b = (1 / b) * bdv" |
|
399 separate_1_bdv_n "bdv ^^^ n / b = (1 / b) * bdv ^^^ n" |
|
400 |
|
401 end |
|
402 |
|
403 |
|
404 |
|
405 |
|
406 |
|
407 |
|