78 (_))" 9) |
78 (_))" 9) |
79 |
79 |
80 (*-------------------- rules -------------------------------------------------*) |
80 (*-------------------- rules -------------------------------------------------*) |
81 axioms |
81 axioms |
82 |
82 |
83 cancel_leading_coeff1 "Not (c =!= 0) ==> (a + b*bdv + c*bdv^^^2 = 0) = |
83 cancel_leading_coeff1: "Not (c =!= 0) ==> (a + b*bdv + c*bdv^^^2 = 0) = |
84 (a/c + b/c*bdv + bdv^^^2 = 0)" |
84 (a/c + b/c*bdv + bdv^^^2 = 0)" |
85 cancel_leading_coeff2 "Not (c =!= 0) ==> (a - b*bdv + c*bdv^^^2 = 0) = |
85 cancel_leading_coeff2: "Not (c =!= 0) ==> (a - b*bdv + c*bdv^^^2 = 0) = |
86 (a/c - b/c*bdv + bdv^^^2 = 0)" |
86 (a/c - b/c*bdv + bdv^^^2 = 0)" |
87 cancel_leading_coeff3 "Not (c =!= 0) ==> (a + b*bdv - c*bdv^^^2 = 0) = |
87 cancel_leading_coeff3: "Not (c =!= 0) ==> (a + b*bdv - c*bdv^^^2 = 0) = |
88 (a/c + b/c*bdv - bdv^^^2 = 0)" |
88 (a/c + b/c*bdv - bdv^^^2 = 0)" |
89 |
89 |
90 cancel_leading_coeff4 "Not (c =!= 0) ==> (a + bdv + c*bdv^^^2 = 0) = |
90 cancel_leading_coeff4: "Not (c =!= 0) ==> (a + bdv + c*bdv^^^2 = 0) = |
91 (a/c + 1/c*bdv + bdv^^^2 = 0)" |
91 (a/c + 1/c*bdv + bdv^^^2 = 0)" |
92 cancel_leading_coeff5 "Not (c =!= 0) ==> (a - bdv + c*bdv^^^2 = 0) = |
92 cancel_leading_coeff5: "Not (c =!= 0) ==> (a - bdv + c*bdv^^^2 = 0) = |
93 (a/c - 1/c*bdv + bdv^^^2 = 0)" |
93 (a/c - 1/c*bdv + bdv^^^2 = 0)" |
94 cancel_leading_coeff6 "Not (c =!= 0) ==> (a + bdv - c*bdv^^^2 = 0) = |
94 cancel_leading_coeff6: "Not (c =!= 0) ==> (a + bdv - c*bdv^^^2 = 0) = |
95 (a/c + 1/c*bdv - bdv^^^2 = 0)" |
95 (a/c + 1/c*bdv - bdv^^^2 = 0)" |
96 |
96 |
97 cancel_leading_coeff7 "Not (c =!= 0) ==> ( b*bdv + c*bdv^^^2 = 0) = |
97 cancel_leading_coeff7: "Not (c =!= 0) ==> ( b*bdv + c*bdv^^^2 = 0) = |
98 ( b/c*bdv + bdv^^^2 = 0)" |
98 ( b/c*bdv + bdv^^^2 = 0)" |
99 cancel_leading_coeff8 "Not (c =!= 0) ==> ( b*bdv - c*bdv^^^2 = 0) = |
99 cancel_leading_coeff8: "Not (c =!= 0) ==> ( b*bdv - c*bdv^^^2 = 0) = |
100 ( b/c*bdv - bdv^^^2 = 0)" |
100 ( b/c*bdv - bdv^^^2 = 0)" |
101 |
101 |
102 cancel_leading_coeff9 "Not (c =!= 0) ==> ( bdv + c*bdv^^^2 = 0) = |
102 cancel_leading_coeff9: "Not (c =!= 0) ==> ( bdv + c*bdv^^^2 = 0) = |
103 ( 1/c*bdv + bdv^^^2 = 0)" |
103 ( 1/c*bdv + bdv^^^2 = 0)" |
104 cancel_leading_coeff10"Not (c =!= 0) ==> ( bdv - c*bdv^^^2 = 0) = |
104 cancel_leading_coeff10:"Not (c =!= 0) ==> ( bdv - c*bdv^^^2 = 0) = |
105 ( 1/c*bdv - bdv^^^2 = 0)" |
105 ( 1/c*bdv - bdv^^^2 = 0)" |
106 |
106 |
107 cancel_leading_coeff11"Not (c =!= 0) ==> (a + b*bdv^^^2 = 0) = |
107 cancel_leading_coeff11:"Not (c =!= 0) ==> (a + b*bdv^^^2 = 0) = |
108 (a/b + bdv^^^2 = 0)" |
108 (a/b + bdv^^^2 = 0)" |
109 cancel_leading_coeff12"Not (c =!= 0) ==> (a - b*bdv^^^2 = 0) = |
109 cancel_leading_coeff12:"Not (c =!= 0) ==> (a - b*bdv^^^2 = 0) = |
110 (a/b - bdv^^^2 = 0)" |
110 (a/b - bdv^^^2 = 0)" |
111 cancel_leading_coeff13"Not (c =!= 0) ==> ( b*bdv^^^2 = 0) = |
111 cancel_leading_coeff13:"Not (c =!= 0) ==> ( b*bdv^^^2 = 0) = |
112 ( bdv^^^2 = 0/b)" |
112 ( bdv^^^2 = 0/b)" |
113 |
113 |
114 complete_square1 "(q + p*bdv + bdv^^^2 = 0) = |
114 complete_square1: "(q + p*bdv + bdv^^^2 = 0) = |
115 (q + (p/2 + bdv)^^^2 = (p/2)^^^2)" |
115 (q + (p/2 + bdv)^^^2 = (p/2)^^^2)" |
116 complete_square2 "( p*bdv + bdv^^^2 = 0) = |
116 complete_square2: "( p*bdv + bdv^^^2 = 0) = |
117 ( (p/2 + bdv)^^^2 = (p/2)^^^2)" |
117 ( (p/2 + bdv)^^^2 = (p/2)^^^2)" |
118 complete_square3 "( bdv + bdv^^^2 = 0) = |
118 complete_square3: "( bdv + bdv^^^2 = 0) = |
119 ( (1/2 + bdv)^^^2 = (1/2)^^^2)" |
119 ( (1/2 + bdv)^^^2 = (1/2)^^^2)" |
120 |
120 |
121 complete_square4 "(q - p*bdv + bdv^^^2 = 0) = |
121 complete_square4: "(q - p*bdv + bdv^^^2 = 0) = |
122 (q + (p/2 - bdv)^^^2 = (p/2)^^^2)" |
122 (q + (p/2 - bdv)^^^2 = (p/2)^^^2)" |
123 complete_square5 "(q + p*bdv - bdv^^^2 = 0) = |
123 complete_square5: "(q + p*bdv - bdv^^^2 = 0) = |
124 (q + (p/2 - bdv)^^^2 = (p/2)^^^2)" |
124 (q + (p/2 - bdv)^^^2 = (p/2)^^^2)" |
125 |
125 |
126 square_explicit1 "(a + b^^^2 = c) = ( b^^^2 = c - a)" |
126 square_explicit1: "(a + b^^^2 = c) = ( b^^^2 = c - a)" |
127 square_explicit2 "(a - b^^^2 = c) = (-(b^^^2) = c - a)" |
127 square_explicit2: "(a - b^^^2 = c) = (-(b^^^2) = c - a)" |
128 |
128 |
129 bdv_explicit1 "(a + bdv = b) = (bdv = - a + b)" |
129 bdv_explicit1: "(a + bdv = b) = (bdv = - a + b)" |
130 bdv_explicit2 "(a - bdv = b) = ((-1)*bdv = - a + b)" |
130 bdv_explicit2: "(a - bdv = b) = ((-1)*bdv = - a + b)" |
131 bdv_explicit3 "((-1)*bdv = b) = (bdv = (-1)*b)" |
131 bdv_explicit3: "((-1)*bdv = b) = (bdv = (-1)*b)" |
132 |
132 |
133 plus_leq "(0 <= a + b) = ((-1)*b <= a)"(*Isa?*) |
133 plus_leq: "(0 <= a + b) = ((-1)*b <= a)"(*Isa?*) |
134 minus_leq "(0 <= a - b) = ( b <= a)"(*Isa?*) |
134 minus_leq: "(0 <= a - b) = ( b <= a)"(*Isa?*) |
135 |
135 |
136 (*-- normalize --*) |
136 (*-- normalize --*) |
137 (*WN0509 compare LinEq.all_left "[|Not(b=!=0)|] ==> (a=b) = (a+(-1)*b=0)"*) |
137 (*WN0509 compare LinEq.all_left "[|Not(b=!=0)|] ==> (a=b) = (a+(-1)*b=0)"*) |
138 all_left "[|Not(b=!=0)|] ==> (a = b) = (a - b = 0)" |
138 all_left: "[|Not(b=!=0)|] ==> (a = b) = (a - b = 0)" |
139 makex1_x "a^^^1 = a" |
139 makex1_x: "a^^^1 = a" |
140 real_assoc_1 "a+(b+c) = a+b+c" |
140 real_assoc_1: "a+(b+c) = a+b+c" |
141 real_assoc_2 "a*(b*c) = a*b*c" |
141 real_assoc_2: "a*(b*c) = a*b*c" |
142 |
142 |
143 (* ---- degree 0 ----*) |
143 (* ---- degree 0 ----*) |
144 d0_true "(0=0) = True" |
144 d0_true: "(0=0) = True" |
145 d0_false "[|Not(bdv occurs_in a);Not(a=0)|] ==> (a=0) = False" |
145 d0_false: "[|Not(bdv occurs_in a);Not(a=0)|] ==> (a=0) = False" |
146 (* ---- degree 1 ----*) |
146 (* ---- degree 1 ----*) |
147 d1_isolate_add1 |
147 d1_isolate_add1: |
148 "[|Not(bdv occurs_in a)|] ==> (a + b*bdv = 0) = (b*bdv = (-1)*a)" |
148 "[|Not(bdv occurs_in a)|] ==> (a + b*bdv = 0) = (b*bdv = (-1)*a)" |
149 d1_isolate_add2 |
149 d1_isolate_add2: |
150 "[|Not(bdv occurs_in a)|] ==> (a + bdv = 0) = ( bdv = (-1)*a)" |
150 "[|Not(bdv occurs_in a)|] ==> (a + bdv = 0) = ( bdv = (-1)*a)" |
151 d1_isolate_div |
151 d1_isolate_div: |
152 "[|Not(b=0);Not(bdv occurs_in c)|] ==> (b*bdv = c) = (bdv = c/b)" |
152 "[|Not(b=0);Not(bdv occurs_in c)|] ==> (b*bdv = c) = (bdv = c/b)" |
153 (* ---- degree 2 ----*) |
153 (* ---- degree 2 ----*) |
154 d2_isolate_add1 |
154 d2_isolate_add1: |
155 "[|Not(bdv occurs_in a)|] ==> (a + b*bdv^^^2=0) = (b*bdv^^^2= (-1)*a)" |
155 "[|Not(bdv occurs_in a)|] ==> (a + b*bdv^^^2=0) = (b*bdv^^^2= (-1)*a)" |
156 d2_isolate_add2 |
156 d2_isolate_add2: |
157 "[|Not(bdv occurs_in a)|] ==> (a + bdv^^^2=0) = ( bdv^^^2= (-1)*a)" |
157 "[|Not(bdv occurs_in a)|] ==> (a + bdv^^^2=0) = ( bdv^^^2= (-1)*a)" |
158 d2_isolate_div |
158 d2_isolate_div: |
159 "[|Not(b=0);Not(bdv occurs_in c)|] ==> (b*bdv^^^2=c) = (bdv^^^2=c/b)" |
159 "[|Not(b=0);Not(bdv occurs_in c)|] ==> (b*bdv^^^2=c) = (bdv^^^2=c/b)" |
160 |
160 |
161 d2_prescind1 "(a*bdv + b*bdv^^^2 = 0) = (bdv*(a +b*bdv)=0)" |
161 d2_prescind1: "(a*bdv + b*bdv^^^2 = 0) = (bdv*(a +b*bdv)=0)" |
162 d2_prescind2 "(a*bdv + bdv^^^2 = 0) = (bdv*(a + bdv)=0)" |
162 d2_prescind2: "(a*bdv + bdv^^^2 = 0) = (bdv*(a + bdv)=0)" |
163 d2_prescind3 "( bdv + b*bdv^^^2 = 0) = (bdv*(1+b*bdv)=0)" |
163 d2_prescind3: "( bdv + b*bdv^^^2 = 0) = (bdv*(1+b*bdv)=0)" |
164 d2_prescind4 "( bdv + bdv^^^2 = 0) = (bdv*(1+ bdv)=0)" |
164 d2_prescind4: "( bdv + bdv^^^2 = 0) = (bdv*(1+ bdv)=0)" |
165 (* eliminate degree 2 *) |
165 (* eliminate degree 2 *) |
166 (* thm for neg arguments in sqroot have postfix _neg *) |
166 (* thm for neg arguments in sqroot have postfix _neg *) |
167 d2_sqrt_equation1 "[|(0<=c);Not(bdv occurs_in c)|] ==> |
167 d2_sqrt_equation1: "[|(0<=c);Not(bdv occurs_in c)|] ==> |
168 (bdv^^^2=c) = ((bdv=sqrt c) | (bdv=(-1)*sqrt c ))" |
168 (bdv^^^2=c) = ((bdv=sqrt c) | (bdv=(-1)*sqrt c ))" |
169 d2_sqrt_equation1_neg |
169 d2_sqrt_equation1_neg: |
170 "[|(c<0);Not(bdv occurs_in c)|] ==> (bdv^^^2=c) = False" |
170 "[|(c<0);Not(bdv occurs_in c)|] ==> (bdv^^^2=c) = False" |
171 d2_sqrt_equation2 "(bdv^^^2=0) = (bdv=0)" |
171 d2_sqrt_equation2: "(bdv^^^2=0) = (bdv=0)" |
172 d2_sqrt_equation3 "(b*bdv^^^2=0) = (bdv=0)" |
172 d2_sqrt_equation3: "(b*bdv^^^2=0) = (bdv=0)" |
173 d2_reduce_equation1 "(bdv*(a +b*bdv)=0) = ((bdv=0)|(a+b*bdv=0))" |
173 d2_reduce_equation1: "(bdv*(a +b*bdv)=0) = ((bdv=0)|(a+b*bdv=0))" |
174 d2_reduce_equation2 "(bdv*(a + bdv)=0) = ((bdv=0)|(a+ bdv=0))" |
174 d2_reduce_equation2: "(bdv*(a + bdv)=0) = ((bdv=0)|(a+ bdv=0))" |
175 d2_pqformula1 "[|0<=p^^^2 - 4*q|] ==> (q+p*bdv+ bdv^^^2=0) = |
175 d2_pqformula1: "[|0<=p^^^2 - 4*q|] ==> (q+p*bdv+ bdv^^^2=0) = |
176 ((bdv= (-1)*(p/2) + sqrt(p^^^2 - 4*q)/2) |
176 ((bdv= (-1)*(p/2) + sqrt(p^^^2 - 4*q)/2) |
177 | (bdv= (-1)*(p/2) - sqrt(p^^^2 - 4*q)/2))" |
177 | (bdv= (-1)*(p/2) - sqrt(p^^^2 - 4*q)/2))" |
178 d2_pqformula1_neg "[|p^^^2 - 4*q<0|] ==> (q+p*bdv+ bdv^^^2=0) = False" |
178 d2_pqformula1_neg: "[|p^^^2 - 4*q<0|] ==> (q+p*bdv+ bdv^^^2=0) = False" |
179 d2_pqformula2 "[|0<=p^^^2 - 4*q|] ==> (q+p*bdv+1*bdv^^^2=0) = |
179 d2_pqformula2: "[|0<=p^^^2 - 4*q|] ==> (q+p*bdv+1*bdv^^^2=0) = |
180 ((bdv= (-1)*(p/2) + sqrt(p^^^2 - 4*q)/2) |
180 ((bdv= (-1)*(p/2) + sqrt(p^^^2 - 4*q)/2) |
181 | (bdv= (-1)*(p/2) - sqrt(p^^^2 - 4*q)/2))" |
181 | (bdv= (-1)*(p/2) - sqrt(p^^^2 - 4*q)/2))" |
182 d2_pqformula2_neg "[|p^^^2 - 4*q<0|] ==> (q+p*bdv+1*bdv^^^2=0) = False" |
182 d2_pqformula2_neg: "[|p^^^2 - 4*q<0|] ==> (q+p*bdv+1*bdv^^^2=0) = False" |
183 d2_pqformula3 "[|0<=1 - 4*q|] ==> (q+ bdv+ bdv^^^2=0) = |
183 d2_pqformula3: "[|0<=1 - 4*q|] ==> (q+ bdv+ bdv^^^2=0) = |
184 ((bdv= (-1)*(1/2) + sqrt(1 - 4*q)/2) |
184 ((bdv= (-1)*(1/2) + sqrt(1 - 4*q)/2) |
185 | (bdv= (-1)*(1/2) - sqrt(1 - 4*q)/2))" |
185 | (bdv= (-1)*(1/2) - sqrt(1 - 4*q)/2))" |
186 d2_pqformula3_neg "[|1 - 4*q<0|] ==> (q+ bdv+ bdv^^^2=0) = False" |
186 d2_pqformula3_neg: "[|1 - 4*q<0|] ==> (q+ bdv+ bdv^^^2=0) = False" |
187 d2_pqformula4 "[|0<=1 - 4*q|] ==> (q+ bdv+1*bdv^^^2=0) = |
187 d2_pqformula4: "[|0<=1 - 4*q|] ==> (q+ bdv+1*bdv^^^2=0) = |
188 ((bdv= (-1)*(1/2) + sqrt(1 - 4*q)/2) |
188 ((bdv= (-1)*(1/2) + sqrt(1 - 4*q)/2) |
189 | (bdv= (-1)*(1/2) - sqrt(1 - 4*q)/2))" |
189 | (bdv= (-1)*(1/2) - sqrt(1 - 4*q)/2))" |
190 d2_pqformula4_neg "[|1 - 4*q<0|] ==> (q+ bdv+1*bdv^^^2=0) = False" |
190 d2_pqformula4_neg: "[|1 - 4*q<0|] ==> (q+ bdv+1*bdv^^^2=0) = False" |
191 d2_pqformula5 "[|0<=p^^^2 - 0|] ==> ( p*bdv+ bdv^^^2=0) = |
191 d2_pqformula5: "[|0<=p^^^2 - 0|] ==> ( p*bdv+ bdv^^^2=0) = |
192 ((bdv= (-1)*(p/2) + sqrt(p^^^2 - 0)/2) |
192 ((bdv= (-1)*(p/2) + sqrt(p^^^2 - 0)/2) |
193 | (bdv= (-1)*(p/2) - sqrt(p^^^2 - 0)/2))" |
193 | (bdv= (-1)*(p/2) - sqrt(p^^^2 - 0)/2))" |
194 (* d2_pqformula5_neg not need p^2 never less zero in R *) |
194 (* d2_pqformula5_neg not need p^2 never less zero in R *) |
195 d2_pqformula6 "[|0<=p^^^2 - 0|] ==> ( p*bdv+1*bdv^^^2=0) = |
195 d2_pqformula6: "[|0<=p^^^2 - 0|] ==> ( p*bdv+1*bdv^^^2=0) = |
196 ((bdv= (-1)*(p/2) + sqrt(p^^^2 - 0)/2) |
196 ((bdv= (-1)*(p/2) + sqrt(p^^^2 - 0)/2) |
197 | (bdv= (-1)*(p/2) - sqrt(p^^^2 - 0)/2))" |
197 | (bdv= (-1)*(p/2) - sqrt(p^^^2 - 0)/2))" |
198 (* d2_pqformula6_neg not need p^2 never less zero in R *) |
198 (* d2_pqformula6_neg not need p^2 never less zero in R *) |
199 d2_pqformula7 "[|0<=1 - 0|] ==> ( bdv+ bdv^^^2=0) = |
199 d2_pqformula7: "[|0<=1 - 0|] ==> ( bdv+ bdv^^^2=0) = |
200 ((bdv= (-1)*(1/2) + sqrt(1 - 0)/2) |
200 ((bdv= (-1)*(1/2) + sqrt(1 - 0)/2) |
201 | (bdv= (-1)*(1/2) - sqrt(1 - 0)/2))" |
201 | (bdv= (-1)*(1/2) - sqrt(1 - 0)/2))" |
202 (* d2_pqformula7_neg not need, because 1<0 ==> False*) |
202 (* d2_pqformula7_neg not need, because 1<0 ==> False*) |
203 d2_pqformula8 "[|0<=1 - 0|] ==> ( bdv+1*bdv^^^2=0) = |
203 d2_pqformula8: "[|0<=1 - 0|] ==> ( bdv+1*bdv^^^2=0) = |
204 ((bdv= (-1)*(1/2) + sqrt(1 - 0)/2) |
204 ((bdv= (-1)*(1/2) + sqrt(1 - 0)/2) |
205 | (bdv= (-1)*(1/2) - sqrt(1 - 0)/2))" |
205 | (bdv= (-1)*(1/2) - sqrt(1 - 0)/2))" |
206 (* d2_pqformula8_neg not need, because 1<0 ==> False*) |
206 (* d2_pqformula8_neg not need, because 1<0 ==> False*) |
207 d2_pqformula9 "[|Not(bdv occurs_in q); 0<= (-1)*4*q|] ==> |
207 d2_pqformula9: "[|Not(bdv occurs_in q); 0<= (-1)*4*q|] ==> |
208 (q+ 1*bdv^^^2=0) = ((bdv= 0 + sqrt(0 - 4*q)/2) |
208 (q+ 1*bdv^^^2=0) = ((bdv= 0 + sqrt(0 - 4*q)/2) |
209 | (bdv= 0 - sqrt(0 - 4*q)/2))" |
209 | (bdv= 0 - sqrt(0 - 4*q)/2))" |
210 d2_pqformula9_neg |
210 d2_pqformula9_neg: |
211 "[|Not(bdv occurs_in q); (-1)*4*q<0|] ==> (q+ 1*bdv^^^2=0) = False" |
211 "[|Not(bdv occurs_in q); (-1)*4*q<0|] ==> (q+ 1*bdv^^^2=0) = False" |
212 d2_pqformula10 |
212 d2_pqformula10: |
213 "[|Not(bdv occurs_in q); 0<= (-1)*4*q|] ==> (q+ bdv^^^2=0) = |
213 "[|Not(bdv occurs_in q); 0<= (-1)*4*q|] ==> (q+ bdv^^^2=0) = |
214 ((bdv= 0 + sqrt(0 - 4*q)/2) |
214 ((bdv= 0 + sqrt(0 - 4*q)/2) |
215 | (bdv= 0 - sqrt(0 - 4*q)/2))" |
215 | (bdv= 0 - sqrt(0 - 4*q)/2))" |
216 d2_pqformula10_neg |
216 d2_pqformula10_neg: |
217 "[|Not(bdv occurs_in q); (-1)*4*q<0|] ==> (q+ bdv^^^2=0) = False" |
217 "[|Not(bdv occurs_in q); (-1)*4*q<0|] ==> (q+ bdv^^^2=0) = False" |
218 d2_abcformula1 |
218 d2_abcformula1: |
219 "[|0<=b^^^2 - 4*a*c|] ==> (c + b*bdv+a*bdv^^^2=0) = |
219 "[|0<=b^^^2 - 4*a*c|] ==> (c + b*bdv+a*bdv^^^2=0) = |
220 ((bdv=( -b + sqrt(b^^^2 - 4*a*c))/(2*a)) |
220 ((bdv=( -b + sqrt(b^^^2 - 4*a*c))/(2*a)) |
221 | (bdv=( -b - sqrt(b^^^2 - 4*a*c))/(2*a)))" |
221 | (bdv=( -b - sqrt(b^^^2 - 4*a*c))/(2*a)))" |
222 d2_abcformula1_neg |
222 d2_abcformula1_neg: |
223 "[|b^^^2 - 4*a*c<0|] ==> (c + b*bdv+a*bdv^^^2=0) = False" |
223 "[|b^^^2 - 4*a*c<0|] ==> (c + b*bdv+a*bdv^^^2=0) = False" |
224 d2_abcformula2 |
224 d2_abcformula2: |
225 "[|0<=1 - 4*a*c|] ==> (c+ bdv+a*bdv^^^2=0) = |
225 "[|0<=1 - 4*a*c|] ==> (c+ bdv+a*bdv^^^2=0) = |
226 ((bdv=( -1 + sqrt(1 - 4*a*c))/(2*a)) |
226 ((bdv=( -1 + sqrt(1 - 4*a*c))/(2*a)) |
227 | (bdv=( -1 - sqrt(1 - 4*a*c))/(2*a)))" |
227 | (bdv=( -1 - sqrt(1 - 4*a*c))/(2*a)))" |
228 d2_abcformula2_neg |
228 d2_abcformula2_neg: |
229 "[|1 - 4*a*c<0|] ==> (c+ bdv+a*bdv^^^2=0) = False" |
229 "[|1 - 4*a*c<0|] ==> (c+ bdv+a*bdv^^^2=0) = False" |
230 d2_abcformula3 |
230 d2_abcformula3: |
231 "[|0<=b^^^2 - 4*1*c|] ==> (c + b*bdv+ bdv^^^2=0) = |
231 "[|0<=b^^^2 - 4*1*c|] ==> (c + b*bdv+ bdv^^^2=0) = |
232 ((bdv=( -b + sqrt(b^^^2 - 4*1*c))/(2*1)) |
232 ((bdv=( -b + sqrt(b^^^2 - 4*1*c))/(2*1)) |
233 | (bdv=( -b - sqrt(b^^^2 - 4*1*c))/(2*1)))" |
233 | (bdv=( -b - sqrt(b^^^2 - 4*1*c))/(2*1)))" |
234 d2_abcformula3_neg |
234 d2_abcformula3_neg: |
235 "[|b^^^2 - 4*1*c<0|] ==> (c + b*bdv+ bdv^^^2=0) = False" |
235 "[|b^^^2 - 4*1*c<0|] ==> (c + b*bdv+ bdv^^^2=0) = False" |
236 d2_abcformula4 |
236 d2_abcformula4: |
237 "[|0<=1 - 4*1*c|] ==> (c + bdv+ bdv^^^2=0) = |
237 "[|0<=1 - 4*1*c|] ==> (c + bdv+ bdv^^^2=0) = |
238 ((bdv=( -1 + sqrt(1 - 4*1*c))/(2*1)) |
238 ((bdv=( -1 + sqrt(1 - 4*1*c))/(2*1)) |
239 | (bdv=( -1 - sqrt(1 - 4*1*c))/(2*1)))" |
239 | (bdv=( -1 - sqrt(1 - 4*1*c))/(2*1)))" |
240 d2_abcformula4_neg |
240 d2_abcformula4_neg: |
241 "[|1 - 4*1*c<0|] ==> (c + bdv+ bdv^^^2=0) = False" |
241 "[|1 - 4*1*c<0|] ==> (c + bdv+ bdv^^^2=0) = False" |
242 d2_abcformula5 |
242 d2_abcformula5: |
243 "[|Not(bdv occurs_in c); 0<=0 - 4*a*c|] ==> (c + a*bdv^^^2=0) = |
243 "[|Not(bdv occurs_in c); 0<=0 - 4*a*c|] ==> (c + a*bdv^^^2=0) = |
244 ((bdv=( 0 + sqrt(0 - 4*a*c))/(2*a)) |
244 ((bdv=( 0 + sqrt(0 - 4*a*c))/(2*a)) |
245 | (bdv=( 0 - sqrt(0 - 4*a*c))/(2*a)))" |
245 | (bdv=( 0 - sqrt(0 - 4*a*c))/(2*a)))" |
246 d2_abcformula5_neg |
246 d2_abcformula5_neg: |
247 "[|Not(bdv occurs_in c); 0 - 4*a*c<0|] ==> (c + a*bdv^^^2=0) = False" |
247 "[|Not(bdv occurs_in c); 0 - 4*a*c<0|] ==> (c + a*bdv^^^2=0) = False" |
248 d2_abcformula6 |
248 d2_abcformula6: |
249 "[|Not(bdv occurs_in c); 0<=0 - 4*1*c|] ==> (c+ bdv^^^2=0) = |
249 "[|Not(bdv occurs_in c); 0<=0 - 4*1*c|] ==> (c+ bdv^^^2=0) = |
250 ((bdv=( 0 + sqrt(0 - 4*1*c))/(2*1)) |
250 ((bdv=( 0 + sqrt(0 - 4*1*c))/(2*1)) |
251 | (bdv=( 0 - sqrt(0 - 4*1*c))/(2*1)))" |
251 | (bdv=( 0 - sqrt(0 - 4*1*c))/(2*1)))" |
252 d2_abcformula6_neg |
252 d2_abcformula6_neg: |
253 "[|Not(bdv occurs_in c); 0 - 4*1*c<0|] ==> (c+ bdv^^^2=0) = False" |
253 "[|Not(bdv occurs_in c); 0 - 4*1*c<0|] ==> (c+ bdv^^^2=0) = False" |
254 d2_abcformula7 |
254 d2_abcformula7: |
255 "[|0<=b^^^2 - 0|] ==> ( b*bdv+a*bdv^^^2=0) = |
255 "[|0<=b^^^2 - 0|] ==> ( b*bdv+a*bdv^^^2=0) = |
256 ((bdv=( -b + sqrt(b^^^2 - 0))/(2*a)) |
256 ((bdv=( -b + sqrt(b^^^2 - 0))/(2*a)) |
257 | (bdv=( -b - sqrt(b^^^2 - 0))/(2*a)))" |
257 | (bdv=( -b - sqrt(b^^^2 - 0))/(2*a)))" |
258 (* d2_abcformula7_neg not need b^2 never less zero in R *) |
258 (* d2_abcformula7_neg not need b^2 never less zero in R *) |
259 d2_abcformula8 |
259 d2_abcformula8: |
260 "[|0<=b^^^2 - 0|] ==> ( b*bdv+ bdv^^^2=0) = |
260 "[|0<=b^^^2 - 0|] ==> ( b*bdv+ bdv^^^2=0) = |
261 ((bdv=( -b + sqrt(b^^^2 - 0))/(2*1)) |
261 ((bdv=( -b + sqrt(b^^^2 - 0))/(2*1)) |
262 | (bdv=( -b - sqrt(b^^^2 - 0))/(2*1)))" |
262 | (bdv=( -b - sqrt(b^^^2 - 0))/(2*1)))" |
263 (* d2_abcformula8_neg not need b^2 never less zero in R *) |
263 (* d2_abcformula8_neg not need b^2 never less zero in R *) |
264 d2_abcformula9 |
264 d2_abcformula9: |
265 "[|0<=1 - 0|] ==> ( bdv+a*bdv^^^2=0) = |
265 "[|0<=1 - 0|] ==> ( bdv+a*bdv^^^2=0) = |
266 ((bdv=( -1 + sqrt(1 - 0))/(2*a)) |
266 ((bdv=( -1 + sqrt(1 - 0))/(2*a)) |
267 | (bdv=( -1 - sqrt(1 - 0))/(2*a)))" |
267 | (bdv=( -1 - sqrt(1 - 0))/(2*a)))" |
268 (* d2_abcformula9_neg not need, because 1<0 ==> False*) |
268 (* d2_abcformula9_neg not need, because 1<0 ==> False*) |
269 d2_abcformula10 |
269 d2_abcformula10: |
270 "[|0<=1 - 0|] ==> ( bdv+ bdv^^^2=0) = |
270 "[|0<=1 - 0|] ==> ( bdv+ bdv^^^2=0) = |
271 ((bdv=( -1 + sqrt(1 - 0))/(2*1)) |
271 ((bdv=( -1 + sqrt(1 - 0))/(2*1)) |
272 | (bdv=( -1 - sqrt(1 - 0))/(2*1)))" |
272 | (bdv=( -1 - sqrt(1 - 0))/(2*1)))" |
273 (* d2_abcformula10_neg not need, because 1<0 ==> False*) |
273 (* d2_abcformula10_neg not need, because 1<0 ==> False*) |
274 |
274 |
275 (* ---- degree 3 ----*) |
275 (* ---- degree 3 ----*) |
276 d3_reduce_equation1 |
276 d3_reduce_equation1: |
277 "(a*bdv + b*bdv^^^2 + c*bdv^^^3=0) = (bdv=0 | (a + b*bdv + c*bdv^^^2=0))" |
277 "(a*bdv + b*bdv^^^2 + c*bdv^^^3=0) = (bdv=0 | (a + b*bdv + c*bdv^^^2=0))" |
278 d3_reduce_equation2 |
278 d3_reduce_equation2: |
279 "( bdv + b*bdv^^^2 + c*bdv^^^3=0) = (bdv=0 | (1 + b*bdv + c*bdv^^^2=0))" |
279 "( bdv + b*bdv^^^2 + c*bdv^^^3=0) = (bdv=0 | (1 + b*bdv + c*bdv^^^2=0))" |
280 d3_reduce_equation3 |
280 d3_reduce_equation3: |
281 "(a*bdv + bdv^^^2 + c*bdv^^^3=0) = (bdv=0 | (a + bdv + c*bdv^^^2=0))" |
281 "(a*bdv + bdv^^^2 + c*bdv^^^3=0) = (bdv=0 | (a + bdv + c*bdv^^^2=0))" |
282 d3_reduce_equation4 |
282 d3_reduce_equation4: |
283 "( bdv + bdv^^^2 + c*bdv^^^3=0) = (bdv=0 | (1 + bdv + c*bdv^^^2=0))" |
283 "( bdv + bdv^^^2 + c*bdv^^^3=0) = (bdv=0 | (1 + bdv + c*bdv^^^2=0))" |
284 d3_reduce_equation5 |
284 d3_reduce_equation5: |
285 "(a*bdv + b*bdv^^^2 + bdv^^^3=0) = (bdv=0 | (a + b*bdv + bdv^^^2=0))" |
285 "(a*bdv + b*bdv^^^2 + bdv^^^3=0) = (bdv=0 | (a + b*bdv + bdv^^^2=0))" |
286 d3_reduce_equation6 |
286 d3_reduce_equation6: |
287 "( bdv + b*bdv^^^2 + bdv^^^3=0) = (bdv=0 | (1 + b*bdv + bdv^^^2=0))" |
287 "( bdv + b*bdv^^^2 + bdv^^^3=0) = (bdv=0 | (1 + b*bdv + bdv^^^2=0))" |
288 d3_reduce_equation7 |
288 d3_reduce_equation7: |
289 "(a*bdv + bdv^^^2 + bdv^^^3=0) = (bdv=0 | (1 + bdv + bdv^^^2=0))" |
289 "(a*bdv + bdv^^^2 + bdv^^^3=0) = (bdv=0 | (1 + bdv + bdv^^^2=0))" |
290 d3_reduce_equation8 |
290 d3_reduce_equation8: |
291 "( bdv + bdv^^^2 + bdv^^^3=0) = (bdv=0 | (1 + bdv + bdv^^^2=0))" |
291 "( bdv + bdv^^^2 + bdv^^^3=0) = (bdv=0 | (1 + bdv + bdv^^^2=0))" |
292 d3_reduce_equation9 |
292 d3_reduce_equation9: |
293 "(a*bdv + c*bdv^^^3=0) = (bdv=0 | (a + c*bdv^^^2=0))" |
293 "(a*bdv + c*bdv^^^3=0) = (bdv=0 | (a + c*bdv^^^2=0))" |
294 d3_reduce_equation10 |
294 d3_reduce_equation10: |
295 "( bdv + c*bdv^^^3=0) = (bdv=0 | (1 + c*bdv^^^2=0))" |
295 "( bdv + c*bdv^^^3=0) = (bdv=0 | (1 + c*bdv^^^2=0))" |
296 d3_reduce_equation11 |
296 d3_reduce_equation11: |
297 "(a*bdv + bdv^^^3=0) = (bdv=0 | (a + bdv^^^2=0))" |
297 "(a*bdv + bdv^^^3=0) = (bdv=0 | (a + bdv^^^2=0))" |
298 d3_reduce_equation12 |
298 d3_reduce_equation12: |
299 "( bdv + bdv^^^3=0) = (bdv=0 | (1 + bdv^^^2=0))" |
299 "( bdv + bdv^^^3=0) = (bdv=0 | (1 + bdv^^^2=0))" |
300 d3_reduce_equation13 |
300 d3_reduce_equation13: |
301 "( b*bdv^^^2 + c*bdv^^^3=0) = (bdv=0 | ( b*bdv + c*bdv^^^2=0))" |
301 "( b*bdv^^^2 + c*bdv^^^3=0) = (bdv=0 | ( b*bdv + c*bdv^^^2=0))" |
302 d3_reduce_equation14 |
302 d3_reduce_equation14: |
303 "( bdv^^^2 + c*bdv^^^3=0) = (bdv=0 | ( bdv + c*bdv^^^2=0))" |
303 "( bdv^^^2 + c*bdv^^^3=0) = (bdv=0 | ( bdv + c*bdv^^^2=0))" |
304 d3_reduce_equation15 |
304 d3_reduce_equation15: |
305 "( b*bdv^^^2 + bdv^^^3=0) = (bdv=0 | ( b*bdv + bdv^^^2=0))" |
305 "( b*bdv^^^2 + bdv^^^3=0) = (bdv=0 | ( b*bdv + bdv^^^2=0))" |
306 d3_reduce_equation16 |
306 d3_reduce_equation16: |
307 "( bdv^^^2 + bdv^^^3=0) = (bdv=0 | ( bdv + bdv^^^2=0))" |
307 "( bdv^^^2 + bdv^^^3=0) = (bdv=0 | ( bdv + bdv^^^2=0))" |
308 d3_isolate_add1 |
308 d3_isolate_add1: |
309 "[|Not(bdv occurs_in a)|] ==> (a + b*bdv^^^3=0) = (b*bdv^^^3= (-1)*a)" |
309 "[|Not(bdv occurs_in a)|] ==> (a + b*bdv^^^3=0) = (b*bdv^^^3= (-1)*a)" |
310 d3_isolate_add2 |
310 d3_isolate_add2: |
311 "[|Not(bdv occurs_in a)|] ==> (a + bdv^^^3=0) = ( bdv^^^3= (-1)*a)" |
311 "[|Not(bdv occurs_in a)|] ==> (a + bdv^^^3=0) = ( bdv^^^3= (-1)*a)" |
312 d3_isolate_div |
312 d3_isolate_div: |
313 "[|Not(b=0);Not(bdv occurs_in a)|] ==> (b*bdv^^^3=c) = (bdv^^^3=c/b)" |
313 "[|Not(b=0);Not(bdv occurs_in a)|] ==> (b*bdv^^^3=c) = (bdv^^^3=c/b)" |
314 d3_root_equation2 |
314 d3_root_equation2: |
315 "(bdv^^^3=0) = (bdv=0)" |
315 "(bdv^^^3=0) = (bdv=0)" |
316 d3_root_equation1 |
316 d3_root_equation1: |
317 "(bdv^^^3=c) = (bdv = nroot 3 c)" |
317 "(bdv^^^3=c) = (bdv = nroot 3 c)" |
318 |
318 |
319 (* ---- degree 4 ----*) |
319 (* ---- degree 4 ----*) |
320 (* RL03.FIXME es wir nicht getestet ob u>0 *) |
320 (* RL03.FIXME es wir nicht getestet ob u>0 *) |
321 d4_sub_u1 |
321 d4_sub_u1 |
322 "(c+b*bdv^^^2+a*bdv^^^4=0) = |
322 "(c+b*bdv^^^2+a*bdv^^^4=0) = |
323 ((a*u^^^2+b*u+c=0) & (bdv^^^2=u))" |
323 ((a*u^^^2+b*u+c=0) & (bdv^^^2=u))" |
324 |
324 |
325 (* ---- 7.3.02 von Termorder ---- *) |
325 (* ---- 7.3.02 von Termorder ---- *) |
326 |
326 |
327 bdv_collect_1 "l * bdv + m * bdv = (l + m) * bdv" |
327 bdv_collect_1: "l * bdv + m * bdv = (l + m) * bdv" |
328 bdv_collect_2 "bdv + m * bdv = (1 + m) * bdv" |
328 bdv_collect_2: "bdv + m * bdv = (1 + m) * bdv" |
329 bdv_collect_3 "l * bdv + bdv = (l + 1) * bdv" |
329 bdv_collect_3: "l * bdv + bdv = (l + 1) * bdv" |
330 |
330 |
331 (* bdv_collect_assoc0_1 "l * bdv + m * bdv + k = (l + m) * bdv + k" |
331 (* bdv_collect_assoc0_1 "l * bdv + m * bdv + k = (l + m) * bdv + k" |
332 bdv_collect_assoc0_2 "bdv + m * bdv + k = (1 + m) * bdv + k" |
332 bdv_collect_assoc0_2 "bdv + m * bdv + k = (1 + m) * bdv + k" |
333 bdv_collect_assoc0_3 "l * bdv + bdv + k = (l + 1) * bdv + k" |
333 bdv_collect_assoc0_3 "l * bdv + bdv + k = (l + 1) * bdv + k" |
334 *) |
334 *) |
335 bdv_collect_assoc1_1 "l * bdv + (m * bdv + k) = (l + m) * bdv + k" |
335 bdv_collect_assoc1_1:"l * bdv + (m * bdv + k) = (l + m) * bdv + k" |
336 bdv_collect_assoc1_2 "bdv + (m * bdv + k) = (1 + m) * bdv + k" |
336 bdv_collect_assoc1_2:"bdv + (m * bdv + k) = (1 + m) * bdv + k" |
337 bdv_collect_assoc1_3 "l * bdv + (bdv + k) = (l + 1) * bdv + k" |
337 bdv_collect_assoc1_3:"l * bdv + (bdv + k) = (l + 1) * bdv + k" |
338 |
338 |
339 bdv_collect_assoc2_1 "k + l * bdv + m * bdv = k + (l + m) * bdv" |
339 bdv_collect_assoc2_1:"k + l * bdv + m * bdv = k + (l + m) * bdv" |
340 bdv_collect_assoc2_2 "k + bdv + m * bdv = k + (1 + m) * bdv" |
340 bdv_collect_assoc2_2:"k + bdv + m * bdv = k + (1 + m) * bdv" |
341 bdv_collect_assoc2_3 "k + l * bdv + bdv = k + (l + 1) * bdv" |
341 bdv_collect_assoc2_3:"k + l * bdv + bdv = k + (l + 1) * bdv" |
342 |
342 |
343 |
343 |
344 bdv_n_collect_1 "l * bdv^^^n + m * bdv^^^n = (l + m) * bdv^^^n" |
344 bdv_n_collect_1: "l * bdv^^^n + m * bdv^^^n = (l + m) * bdv^^^n" |
345 bdv_n_collect_2 " bdv^^^n + m * bdv^^^n = (1 + m) * bdv^^^n" |
345 bdv_n_collect_2: " bdv^^^n + m * bdv^^^n = (1 + m) * bdv^^^n" |
346 bdv_n_collect_3 "l * bdv^^^n + bdv^^^n = (l + 1) * bdv^^^n" (*order!*) |
346 bdv_n_collect_3: "l * bdv^^^n + bdv^^^n = (l + 1) * bdv^^^n" (*order!*) |
347 |
347 |
348 bdv_n_collect_assoc1_1 "l * bdv^^^n + (m * bdv^^^n + k) = (l + m) * bdv^^^n + k" |
348 bdv_n_collect_assoc1_1:"l * bdv^^^n + (m * bdv^^^n + k) = (l + m) * bdv^^^n + k" |
349 bdv_n_collect_assoc1_2 "bdv^^^n + (m * bdv^^^n + k) = (1 + m) * bdv^^^n + k" |
349 bdv_n_collect_assoc1_2:"bdv^^^n + (m * bdv^^^n + k) = (1 + m) * bdv^^^n + k" |
350 bdv_n_collect_assoc1_3 "l * bdv^^^n + (bdv^^^n + k) = (l + 1) * bdv^^^n + k" |
350 bdv_n_collect_assoc1_3:"l * bdv^^^n + (bdv^^^n + k) = (l + 1) * bdv^^^n + k" |
351 |
351 |
352 bdv_n_collect_assoc2_1 "k + l * bdv^^^n + m * bdv^^^n = k + (l + m) * bdv^^^n" |
352 bdv_n_collect_assoc2_1:"k + l * bdv^^^n + m * bdv^^^n = k + (l + m) * bdv^^^n" |
353 bdv_n_collect_assoc2_2 "k + bdv^^^n + m * bdv^^^n = k + (1 + m) * bdv^^^n" |
353 bdv_n_collect_assoc2_2:"k + bdv^^^n + m * bdv^^^n = k + (1 + m) * bdv^^^n" |
354 bdv_n_collect_assoc2_3 "k + l * bdv^^^n + bdv^^^n = k + (l + 1) * bdv^^^n" |
354 bdv_n_collect_assoc2_3:"k + l * bdv^^^n + bdv^^^n = k + (l + 1) * bdv^^^n" |
355 |
355 |
356 (*WN.14.3.03*) |
356 (*WN.14.3.03*) |
357 real_minus_div "- (a / b) = (-1 * a) / b" |
357 real_minus_div: "- (a / b) = (-1 * a) / b" |
358 |
358 |
359 separate_bdv "(a * bdv) / b = (a / b) * bdv" |
359 separate_bdv: "(a * bdv) / b = (a / b) * bdv" |
360 separate_bdv_n "(a * bdv ^^^ n) / b = (a / b) * bdv ^^^ n" |
360 separate_bdv_n: "(a * bdv ^^^ n) / b = (a / b) * bdv ^^^ n" |
361 separate_1_bdv "bdv / b = (1 / b) * bdv" |
361 separate_1_bdv: "bdv / b = (1 / b) * bdv" |
362 separate_1_bdv_n "bdv ^^^ n / b = (1 / b) * bdv ^^^ n" |
362 separate_1_bdv_n: "bdv ^^^ n / b = (1 / b) * bdv ^^^ n" |
363 |
363 |
364 ML {* |
364 ML {* |
365 val thy = @{theory}; |
365 val thy = @{theory}; |
366 |
366 |
367 (*-------------------------rulse-------------------------*) |
367 (*-------------------------rulse-------------------------*) |