1.1 --- a/src/Tools/isac/IsacKnowledge/PolyEq.thy Wed Aug 25 15:15:01 2010 +0200
1.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
1.3 @@ -1,407 +0,0 @@
1.4 -(*.(c) by Richard Lang, 2003 .*)
1.5 -(* theory collecting all knowledge
1.6 - (predicates 'is_rootEq_in', 'is_sqrt_in', 'is_ratEq_in')
1.7 - for PolynomialEquations.
1.8 - alternative dependencies see Isac.thy
1.9 - created by: rlang
1.10 - date: 02.07
1.11 - changed by: rlang
1.12 - last change by: rlang
1.13 - date: 03.06.03
1.14 -*)
1.15 -
1.16 -(* remove_thy"PolyEq";
1.17 - use_thy"IsacKnowledge/Isac";
1.18 - use_thy"IsacKnowledge/PolyEq";
1.19 -
1.20 - remove_thy"PolyEq";
1.21 - use_thy"Isac";
1.22 -
1.23 - use"ROOT.ML";
1.24 - cd"knowledge";
1.25 - *)
1.26 -
1.27 -PolyEq = LinEq + RootRatEq +
1.28 -(*-------------------- consts ------------------------------------------------*)
1.29 -consts
1.30 -
1.31 -(*---------scripts--------------------------*)
1.32 - Complete'_square
1.33 - :: "[bool,real, \
1.34 - \ bool list] => bool list"
1.35 - ("((Script Complete'_square (_ _ =))// \
1.36 - \ (_))" 9)
1.37 - (*----- poly ----- *)
1.38 - Normalize'_poly
1.39 - :: "[bool,real, \
1.40 - \ bool list] => bool list"
1.41 - ("((Script Normalize'_poly (_ _=))// \
1.42 - \ (_))" 9)
1.43 - Solve'_d0'_polyeq'_equation
1.44 - :: "[bool,real, \
1.45 - \ bool list] => bool list"
1.46 - ("((Script Solve'_d0'_polyeq'_equation (_ _ =))// \
1.47 - \ (_))" 9)
1.48 - Solve'_d1'_polyeq'_equation
1.49 - :: "[bool,real, \
1.50 - \ bool list] => bool list"
1.51 - ("((Script Solve'_d1'_polyeq'_equation (_ _ =))// \
1.52 - \ (_))" 9)
1.53 - Solve'_d2'_polyeq'_equation
1.54 - :: "[bool,real, \
1.55 - \ bool list] => bool list"
1.56 - ("((Script Solve'_d2'_polyeq'_equation (_ _ =))// \
1.57 - \ (_))" 9)
1.58 - Solve'_d2'_polyeq'_sqonly'_equation
1.59 - :: "[bool,real, \
1.60 - \ bool list] => bool list"
1.61 - ("((Script Solve'_d2'_polyeq'_sqonly'_equation (_ _ =))// \
1.62 - \ (_))" 9)
1.63 - Solve'_d2'_polyeq'_bdvonly'_equation
1.64 - :: "[bool,real, \
1.65 - \ bool list] => bool list"
1.66 - ("((Script Solve'_d2'_polyeq'_bdvonly'_equation (_ _ =))// \
1.67 - \ (_))" 9)
1.68 - Solve'_d2'_polyeq'_pq'_equation
1.69 - :: "[bool,real, \
1.70 - \ bool list] => bool list"
1.71 - ("((Script Solve'_d2'_polyeq'_pq'_equation (_ _ =))// \
1.72 - \ (_))" 9)
1.73 - Solve'_d2'_polyeq'_abc'_equation
1.74 - :: "[bool,real, \
1.75 - \ bool list] => bool list"
1.76 - ("((Script Solve'_d2'_polyeq'_abc'_equation (_ _ =))// \
1.77 - \ (_))" 9)
1.78 - Solve'_d3'_polyeq'_equation
1.79 - :: "[bool,real, \
1.80 - \ bool list] => bool list"
1.81 - ("((Script Solve'_d3'_polyeq'_equation (_ _ =))// \
1.82 - \ (_))" 9)
1.83 - Solve'_d4'_polyeq'_equation
1.84 - :: "[bool,real, \
1.85 - \ bool list] => bool list"
1.86 - ("((Script Solve'_d4'_polyeq'_equation (_ _ =))// \
1.87 - \ (_))" 9)
1.88 - Biquadrat'_poly
1.89 - :: "[bool,real, \
1.90 - \ bool list] => bool list"
1.91 - ("((Script Biquadrat'_poly (_ _=))// \
1.92 - \ (_))" 9)
1.93 -
1.94 -(*-------------------- rules -------------------------------------------------*)
1.95 -rules
1.96 -
1.97 - cancel_leading_coeff1 "Not (c =!= 0) ==> (a + b*bdv + c*bdv^^^2 = 0) = \
1.98 - \ (a/c + b/c*bdv + bdv^^^2 = 0)"
1.99 - cancel_leading_coeff2 "Not (c =!= 0) ==> (a - b*bdv + c*bdv^^^2 = 0) = \
1.100 - \ (a/c - b/c*bdv + bdv^^^2 = 0)"
1.101 - cancel_leading_coeff3 "Not (c =!= 0) ==> (a + b*bdv - c*bdv^^^2 = 0) = \
1.102 - \ (a/c + b/c*bdv - bdv^^^2 = 0)"
1.103 -
1.104 - cancel_leading_coeff4 "Not (c =!= 0) ==> (a + bdv + c*bdv^^^2 = 0) = \
1.105 - \ (a/c + 1/c*bdv + bdv^^^2 = 0)"
1.106 - cancel_leading_coeff5 "Not (c =!= 0) ==> (a - bdv + c*bdv^^^2 = 0) = \
1.107 - \ (a/c - 1/c*bdv + bdv^^^2 = 0)"
1.108 - cancel_leading_coeff6 "Not (c =!= 0) ==> (a + bdv - c*bdv^^^2 = 0) = \
1.109 - \ (a/c + 1/c*bdv - bdv^^^2 = 0)"
1.110 -
1.111 - cancel_leading_coeff7 "Not (c =!= 0) ==> ( b*bdv + c*bdv^^^2 = 0) = \
1.112 - \ ( b/c*bdv + bdv^^^2 = 0)"
1.113 - cancel_leading_coeff8 "Not (c =!= 0) ==> ( b*bdv - c*bdv^^^2 = 0) = \
1.114 - \ ( b/c*bdv - bdv^^^2 = 0)"
1.115 -
1.116 - cancel_leading_coeff9 "Not (c =!= 0) ==> ( bdv + c*bdv^^^2 = 0) = \
1.117 - \ ( 1/c*bdv + bdv^^^2 = 0)"
1.118 - cancel_leading_coeff10"Not (c =!= 0) ==> ( bdv - c*bdv^^^2 = 0) = \
1.119 - \ ( 1/c*bdv - bdv^^^2 = 0)"
1.120 -
1.121 - cancel_leading_coeff11"Not (c =!= 0) ==> (a + b*bdv^^^2 = 0) = \
1.122 - \ (a/b + bdv^^^2 = 0)"
1.123 - cancel_leading_coeff12"Not (c =!= 0) ==> (a - b*bdv^^^2 = 0) = \
1.124 - \ (a/b - bdv^^^2 = 0)"
1.125 - cancel_leading_coeff13"Not (c =!= 0) ==> ( b*bdv^^^2 = 0) = \
1.126 - \ ( bdv^^^2 = 0/b)"
1.127 -
1.128 - complete_square1 "(q + p*bdv + bdv^^^2 = 0) = \
1.129 - \(q + (p/2 + bdv)^^^2 = (p/2)^^^2)"
1.130 - complete_square2 "( p*bdv + bdv^^^2 = 0) = \
1.131 - \( (p/2 + bdv)^^^2 = (p/2)^^^2)"
1.132 - complete_square3 "( bdv + bdv^^^2 = 0) = \
1.133 - \( (1/2 + bdv)^^^2 = (1/2)^^^2)"
1.134 -
1.135 - complete_square4 "(q - p*bdv + bdv^^^2 = 0) = \
1.136 - \(q + (p/2 - bdv)^^^2 = (p/2)^^^2)"
1.137 - complete_square5 "(q + p*bdv - bdv^^^2 = 0) = \
1.138 - \(q + (p/2 - bdv)^^^2 = (p/2)^^^2)"
1.139 -
1.140 - square_explicit1 "(a + b^^^2 = c) = ( b^^^2 = c - a)"
1.141 - square_explicit2 "(a - b^^^2 = c) = (-(b^^^2) = c - a)"
1.142 -
1.143 - bdv_explicit1 "(a + bdv = b) = (bdv = - a + b)"
1.144 - bdv_explicit2 "(a - bdv = b) = ((-1)*bdv = - a + b)"
1.145 - bdv_explicit3 "((-1)*bdv = b) = (bdv = (-1)*b)"
1.146 -
1.147 - plus_leq "(0 <= a + b) = ((-1)*b <= a)"(*Isa?*)
1.148 - minus_leq "(0 <= a - b) = ( b <= a)"(*Isa?*)
1.149 -
1.150 -(*-- normalize --*)
1.151 - (*WN0509 compare LinEq.all_left "[|Not(b=!=0)|] ==> (a=b) = (a+(-1)*b=0)"*)
1.152 - all_left
1.153 - "[|Not(b=!=0)|] ==> (a = b) = (a - b = 0)"
1.154 - makex1_x
1.155 - "a^^^1 = a"
1.156 - real_assoc_1
1.157 - "a+(b+c) = a+b+c"
1.158 - real_assoc_2
1.159 - "a*(b*c) = a*b*c"
1.160 -
1.161 -(* ---- degree 0 ----*)
1.162 - d0_true
1.163 - "(0=0) = True"
1.164 - d0_false
1.165 - "[|Not(bdv occurs_in a);Not(a=0)|] ==> (a=0) = False"
1.166 -(* ---- degree 1 ----*)
1.167 - d1_isolate_add1
1.168 - "[|Not(bdv occurs_in a)|] ==> (a + b*bdv = 0) = (b*bdv = (-1)*a)"
1.169 - d1_isolate_add2
1.170 - "[|Not(bdv occurs_in a)|] ==> (a + bdv = 0) = ( bdv = (-1)*a)"
1.171 - d1_isolate_div
1.172 - "[|Not(b=0);Not(bdv occurs_in c)|] ==> (b*bdv = c) = (bdv = c/b)"
1.173 -(* ---- degree 2 ----*)
1.174 - d2_isolate_add1
1.175 - "[|Not(bdv occurs_in a)|] ==> (a + b*bdv^^^2=0) = (b*bdv^^^2= (-1)*a)"
1.176 - d2_isolate_add2
1.177 - "[|Not(bdv occurs_in a)|] ==> (a + bdv^^^2=0) = ( bdv^^^2= (-1)*a)"
1.178 - d2_isolate_div
1.179 - "[|Not(b=0);Not(bdv occurs_in c)|] ==> (b*bdv^^^2=c) = (bdv^^^2=c/b)"
1.180 - d2_prescind1
1.181 - "(a*bdv + b*bdv^^^2 = 0) = (bdv*(a +b*bdv)=0)"
1.182 - d2_prescind2
1.183 - "(a*bdv + bdv^^^2 = 0) = (bdv*(a + bdv)=0)"
1.184 - d2_prescind3
1.185 - "( bdv + b*bdv^^^2 = 0) = (bdv*(1+b*bdv)=0)"
1.186 - d2_prescind4
1.187 - "( bdv + bdv^^^2 = 0) = (bdv*(1+ bdv)=0)"
1.188 - (* eliminate degree 2 *)
1.189 - (* thm for neg arguments in sqroot have postfix _neg *)
1.190 - d2_sqrt_equation1
1.191 - "[|(0<=c);Not(bdv occurs_in c)|] ==> (bdv^^^2=c) = ((bdv=sqrt c) | (bdv=(-1)*sqrt c ))"
1.192 - d2_sqrt_equation1_neg
1.193 - "[|(c<0);Not(bdv occurs_in c)|] ==> (bdv^^^2=c) = False"
1.194 - d2_sqrt_equation2
1.195 - "(bdv^^^2=0) = (bdv=0)"
1.196 - d2_sqrt_equation3
1.197 - "(b*bdv^^^2=0) = (bdv=0)"
1.198 - d2_reduce_equation1
1.199 - "(bdv*(a +b*bdv)=0) = ((bdv=0)|(a+b*bdv=0))"
1.200 - d2_reduce_equation2
1.201 - "(bdv*(a + bdv)=0) = ((bdv=0)|(a+ bdv=0))"
1.202 - d2_pqformula1
1.203 - "[|0<=p^^^2 - 4*q|] ==> (q+p*bdv+ bdv^^^2=0) =
1.204 - ((bdv= (-1)*(p/2) + sqrt(p^^^2 - 4*q)/2)
1.205 - | (bdv= (-1)*(p/2) - sqrt(p^^^2 - 4*q)/2))"
1.206 - d2_pqformula1_neg
1.207 - "[|p^^^2 - 4*q<0|] ==> (q+p*bdv+ bdv^^^2=0) = False"
1.208 - d2_pqformula2
1.209 - "[|0<=p^^^2 - 4*q|] ==> (q+p*bdv+1*bdv^^^2=0) =
1.210 - ((bdv= (-1)*(p/2) + sqrt(p^^^2 - 4*q)/2)
1.211 - | (bdv= (-1)*(p/2) - sqrt(p^^^2 - 4*q)/2))"
1.212 - d2_pqformula2_neg
1.213 - "[|p^^^2 - 4*q<0|] ==> (q+p*bdv+1*bdv^^^2=0) = False"
1.214 - d2_pqformula3
1.215 - "[|0<=1 - 4*q|] ==> (q+ bdv+ bdv^^^2=0) =
1.216 - ((bdv= (-1)*(1/2) + sqrt(1 - 4*q)/2)
1.217 - | (bdv= (-1)*(1/2) - sqrt(1 - 4*q)/2))"
1.218 - d2_pqformula3_neg
1.219 - "[|1 - 4*q<0|] ==> (q+ bdv+ bdv^^^2=0) = False"
1.220 - d2_pqformula4
1.221 - "[|0<=1 - 4*q|] ==> (q+ bdv+1*bdv^^^2=0) =
1.222 - ((bdv= (-1)*(1/2) + sqrt(1 - 4*q)/2)
1.223 - | (bdv= (-1)*(1/2) - sqrt(1 - 4*q)/2))"
1.224 - d2_pqformula4_neg
1.225 - "[|1 - 4*q<0|] ==> (q+ bdv+1*bdv^^^2=0) = False"
1.226 - d2_pqformula5
1.227 - "[|0<=p^^^2 - 0|] ==> ( p*bdv+ bdv^^^2=0) =
1.228 - ((bdv= (-1)*(p/2) + sqrt(p^^^2 - 0)/2)
1.229 - | (bdv= (-1)*(p/2) - sqrt(p^^^2 - 0)/2))"
1.230 - (* d2_pqformula5_neg not need p^2 never less zero in R *)
1.231 - d2_pqformula6
1.232 - "[|0<=p^^^2 - 0|] ==> ( p*bdv+1*bdv^^^2=0) =
1.233 - ((bdv= (-1)*(p/2) + sqrt(p^^^2 - 0)/2)
1.234 - | (bdv= (-1)*(p/2) - sqrt(p^^^2 - 0)/2))"
1.235 - (* d2_pqformula6_neg not need p^2 never less zero in R *)
1.236 - d2_pqformula7
1.237 - "[|0<=1 - 0|] ==> ( bdv+ bdv^^^2=0) =
1.238 - ((bdv= (-1)*(1/2) + sqrt(1 - 0)/2)
1.239 - | (bdv= (-1)*(1/2) - sqrt(1 - 0)/2))"
1.240 - (* d2_pqformula7_neg not need, because 1<0 ==> False*)
1.241 - d2_pqformula8
1.242 - "[|0<=1 - 0|] ==> ( bdv+1*bdv^^^2=0) =
1.243 - ((bdv= (-1)*(1/2) + sqrt(1 - 0)/2)
1.244 - | (bdv= (-1)*(1/2) - sqrt(1 - 0)/2))"
1.245 - (* d2_pqformula8_neg not need, because 1<0 ==> False*)
1.246 - d2_pqformula9
1.247 - "[|Not(bdv occurs_in q); 0<= (-1)*4*q|] ==> (q+ 1*bdv^^^2=0) =
1.248 - ((bdv= 0 + sqrt(0 - 4*q)/2)
1.249 - | (bdv= 0 - sqrt(0 - 4*q)/2))"
1.250 - d2_pqformula9_neg
1.251 - "[|Not(bdv occurs_in q); (-1)*4*q<0|] ==> (q+ 1*bdv^^^2=0) = False"
1.252 - d2_pqformula10
1.253 - "[|Not(bdv occurs_in q); 0<= (-1)*4*q|] ==> (q+ bdv^^^2=0) =
1.254 - ((bdv= 0 + sqrt(0 - 4*q)/2)
1.255 - | (bdv= 0 - sqrt(0 - 4*q)/2))"
1.256 - d2_pqformula10_neg
1.257 - "[|Not(bdv occurs_in q); (-1)*4*q<0|] ==> (q+ bdv^^^2=0) = False"
1.258 - d2_abcformula1
1.259 - "[|0<=b^^^2 - 4*a*c|] ==> (c + b*bdv+a*bdv^^^2=0) =
1.260 - ((bdv=( -b + sqrt(b^^^2 - 4*a*c))/(2*a))
1.261 - | (bdv=( -b - sqrt(b^^^2 - 4*a*c))/(2*a)))"
1.262 - d2_abcformula1_neg
1.263 - "[|b^^^2 - 4*a*c<0|] ==> (c + b*bdv+a*bdv^^^2=0) = False"
1.264 - d2_abcformula2
1.265 - "[|0<=1 - 4*a*c|] ==> (c+ bdv+a*bdv^^^2=0) =
1.266 - ((bdv=( -1 + sqrt(1 - 4*a*c))/(2*a))
1.267 - | (bdv=( -1 - sqrt(1 - 4*a*c))/(2*a)))"
1.268 - d2_abcformula2_neg
1.269 - "[|1 - 4*a*c<0|] ==> (c+ bdv+a*bdv^^^2=0) = False"
1.270 - d2_abcformula3
1.271 - "[|0<=b^^^2 - 4*1*c|] ==> (c + b*bdv+ bdv^^^2=0) =
1.272 - ((bdv=( -b + sqrt(b^^^2 - 4*1*c))/(2*1))
1.273 - | (bdv=( -b - sqrt(b^^^2 - 4*1*c))/(2*1)))"
1.274 - d2_abcformula3_neg
1.275 - "[|b^^^2 - 4*1*c<0|] ==> (c + b*bdv+ bdv^^^2=0) = False"
1.276 - d2_abcformula4
1.277 - "[|0<=1 - 4*1*c|] ==> (c + bdv+ bdv^^^2=0) =
1.278 - ((bdv=( -1 + sqrt(1 - 4*1*c))/(2*1))
1.279 - | (bdv=( -1 - sqrt(1 - 4*1*c))/(2*1)))"
1.280 - d2_abcformula4_neg
1.281 - "[|1 - 4*1*c<0|] ==> (c + bdv+ bdv^^^2=0) = False"
1.282 - d2_abcformula5
1.283 - "[|Not(bdv occurs_in c); 0<=0 - 4*a*c|] ==> (c + a*bdv^^^2=0) =
1.284 - ((bdv=( 0 + sqrt(0 - 4*a*c))/(2*a))
1.285 - | (bdv=( 0 - sqrt(0 - 4*a*c))/(2*a)))"
1.286 - d2_abcformula5_neg
1.287 - "[|Not(bdv occurs_in c); 0 - 4*a*c<0|] ==> (c + a*bdv^^^2=0) = False"
1.288 - d2_abcformula6
1.289 - "[|Not(bdv occurs_in c); 0<=0 - 4*1*c|] ==> (c+ bdv^^^2=0) =
1.290 - ((bdv=( 0 + sqrt(0 - 4*1*c))/(2*1))
1.291 - | (bdv=( 0 - sqrt(0 - 4*1*c))/(2*1)))"
1.292 - d2_abcformula6_neg
1.293 - "[|Not(bdv occurs_in c); 0 - 4*1*c<0|] ==> (c+ bdv^^^2=0) = False"
1.294 - d2_abcformula7
1.295 - "[|0<=b^^^2 - 0|] ==> ( b*bdv+a*bdv^^^2=0) =
1.296 - ((bdv=( -b + sqrt(b^^^2 - 0))/(2*a))
1.297 - | (bdv=( -b - sqrt(b^^^2 - 0))/(2*a)))"
1.298 - (* d2_abcformula7_neg not need b^2 never less zero in R *)
1.299 - d2_abcformula8
1.300 - "[|0<=b^^^2 - 0|] ==> ( b*bdv+ bdv^^^2=0) =
1.301 - ((bdv=( -b + sqrt(b^^^2 - 0))/(2*1))
1.302 - | (bdv=( -b - sqrt(b^^^2 - 0))/(2*1)))"
1.303 - (* d2_abcformula8_neg not need b^2 never less zero in R *)
1.304 - d2_abcformula9
1.305 - "[|0<=1 - 0|] ==> ( bdv+a*bdv^^^2=0) =
1.306 - ((bdv=( -1 + sqrt(1 - 0))/(2*a))
1.307 - | (bdv=( -1 - sqrt(1 - 0))/(2*a)))"
1.308 - (* d2_abcformula9_neg not need, because 1<0 ==> False*)
1.309 - d2_abcformula10
1.310 - "[|0<=1 - 0|] ==> ( bdv+ bdv^^^2=0) =
1.311 - ((bdv=( -1 + sqrt(1 - 0))/(2*1))
1.312 - | (bdv=( -1 - sqrt(1 - 0))/(2*1)))"
1.313 - (* d2_abcformula10_neg not need, because 1<0 ==> False*)
1.314 -
1.315 -(* ---- degree 3 ----*)
1.316 - d3_reduce_equation1
1.317 - "(a*bdv + b*bdv^^^2 + c*bdv^^^3=0) = (bdv=0 | (a + b*bdv + c*bdv^^^2=0))"
1.318 - d3_reduce_equation2
1.319 - "( bdv + b*bdv^^^2 + c*bdv^^^3=0) = (bdv=0 | (1 + b*bdv + c*bdv^^^2=0))"
1.320 - d3_reduce_equation3
1.321 - "(a*bdv + bdv^^^2 + c*bdv^^^3=0) = (bdv=0 | (a + bdv + c*bdv^^^2=0))"
1.322 - d3_reduce_equation4
1.323 - "( bdv + bdv^^^2 + c*bdv^^^3=0) = (bdv=0 | (1 + bdv + c*bdv^^^2=0))"
1.324 - d3_reduce_equation5
1.325 - "(a*bdv + b*bdv^^^2 + bdv^^^3=0) = (bdv=0 | (a + b*bdv + bdv^^^2=0))"
1.326 - d3_reduce_equation6
1.327 - "( bdv + b*bdv^^^2 + bdv^^^3=0) = (bdv=0 | (1 + b*bdv + bdv^^^2=0))"
1.328 - d3_reduce_equation7
1.329 - "(a*bdv + bdv^^^2 + bdv^^^3=0) = (bdv=0 | (1 + bdv + bdv^^^2=0))"
1.330 - d3_reduce_equation8
1.331 - "( bdv + bdv^^^2 + bdv^^^3=0) = (bdv=0 | (1 + bdv + bdv^^^2=0))"
1.332 - d3_reduce_equation9
1.333 - "(a*bdv + c*bdv^^^3=0) = (bdv=0 | (a + c*bdv^^^2=0))"
1.334 - d3_reduce_equation10
1.335 - "( bdv + c*bdv^^^3=0) = (bdv=0 | (1 + c*bdv^^^2=0))"
1.336 - d3_reduce_equation11
1.337 - "(a*bdv + bdv^^^3=0) = (bdv=0 | (a + bdv^^^2=0))"
1.338 - d3_reduce_equation12
1.339 - "( bdv + bdv^^^3=0) = (bdv=0 | (1 + bdv^^^2=0))"
1.340 - d3_reduce_equation13
1.341 - "( b*bdv^^^2 + c*bdv^^^3=0) = (bdv=0 | ( b*bdv + c*bdv^^^2=0))"
1.342 - d3_reduce_equation14
1.343 - "( bdv^^^2 + c*bdv^^^3=0) = (bdv=0 | ( bdv + c*bdv^^^2=0))"
1.344 - d3_reduce_equation15
1.345 - "( b*bdv^^^2 + bdv^^^3=0) = (bdv=0 | ( b*bdv + bdv^^^2=0))"
1.346 - d3_reduce_equation16
1.347 - "( bdv^^^2 + bdv^^^3=0) = (bdv=0 | ( bdv + bdv^^^2=0))"
1.348 - d3_isolate_add1
1.349 - "[|Not(bdv occurs_in a)|] ==> (a + b*bdv^^^3=0) = (b*bdv^^^3= (-1)*a)"
1.350 - d3_isolate_add2
1.351 - "[|Not(bdv occurs_in a)|] ==> (a + bdv^^^3=0) = ( bdv^^^3= (-1)*a)"
1.352 - d3_isolate_div
1.353 - "[|Not(b=0);Not(bdv occurs_in a)|] ==> (b*bdv^^^3=c) = (bdv^^^3=c/b)"
1.354 - d3_root_equation2
1.355 - "(bdv^^^3=0) = (bdv=0)"
1.356 - d3_root_equation1
1.357 - "(bdv^^^3=c) = (bdv = nroot 3 c)"
1.358 -
1.359 -(* ---- degree 4 ----*)
1.360 - (* RL03.FIXME es wir nicht getestet ob u>0 *)
1.361 - d4_sub_u1
1.362 - "(c+b*bdv^^^2+a*bdv^^^4=0) =
1.363 - ((a*u^^^2+b*u+c=0) & (bdv^^^2=u))"
1.364 -
1.365 -(* ---- 7.3.02 von Termorder ---- *)
1.366 -
1.367 - bdv_collect_1 "l * bdv + m * bdv = (l + m) * bdv"
1.368 - bdv_collect_2 "bdv + m * bdv = (1 + m) * bdv"
1.369 - bdv_collect_3 "l * bdv + bdv = (l + 1) * bdv"
1.370 -
1.371 -(* bdv_collect_assoc0_1 "l * bdv + m * bdv + k = (l + m) * bdv + k"
1.372 - bdv_collect_assoc0_2 "bdv + m * bdv + k = (1 + m) * bdv + k"
1.373 - bdv_collect_assoc0_3 "l * bdv + bdv + k = (l + 1) * bdv + k"
1.374 -*)
1.375 - bdv_collect_assoc1_1 "l * bdv + (m * bdv + k) = (l + m) * bdv + k"
1.376 - bdv_collect_assoc1_2 "bdv + (m * bdv + k) = (1 + m) * bdv + k"
1.377 - bdv_collect_assoc1_3 "l * bdv + (bdv + k) = (l + 1) * bdv + k"
1.378 -
1.379 - bdv_collect_assoc2_1 "k + l * bdv + m * bdv = k + (l + m) * bdv"
1.380 - bdv_collect_assoc2_2 "k + bdv + m * bdv = k + (1 + m) * bdv"
1.381 - bdv_collect_assoc2_3 "k + l * bdv + bdv = k + (l + 1) * bdv"
1.382 -
1.383 -
1.384 - bdv_n_collect_1 "l * bdv^^^n + m * bdv^^^n = (l + m) * bdv^^^n"
1.385 - bdv_n_collect_2 " bdv^^^n + m * bdv^^^n = (1 + m) * bdv^^^n"
1.386 - bdv_n_collect_3 "l * bdv^^^n + bdv^^^n = (l + 1) * bdv^^^n" (*order!*)
1.387 -
1.388 - bdv_n_collect_assoc1_1 "l * bdv^^^n + (m * bdv^^^n + k) = (l + m) * bdv^^^n + k"
1.389 - bdv_n_collect_assoc1_2 "bdv^^^n + (m * bdv^^^n + k) = (1 + m) * bdv^^^n + k"
1.390 - bdv_n_collect_assoc1_3 "l * bdv^^^n + (bdv^^^n + k) = (l + 1) * bdv^^^n + k"
1.391 -
1.392 - bdv_n_collect_assoc2_1 "k + l * bdv^^^n + m * bdv^^^n = k + (l + m) * bdv^^^n"
1.393 - bdv_n_collect_assoc2_2 "k + bdv^^^n + m * bdv^^^n = k + (1 + m) * bdv^^^n"
1.394 - bdv_n_collect_assoc2_3 "k + l * bdv^^^n + bdv^^^n = k + (l + 1) * bdv^^^n"
1.395 -
1.396 -(*WN.14.3.03*)
1.397 - real_minus_div "- (a / b) = (-1 * a) / b"
1.398 -
1.399 - separate_bdv "(a * bdv) / b = (a / b) * bdv"
1.400 - separate_bdv_n "(a * bdv ^^^ n) / b = (a / b) * bdv ^^^ n"
1.401 - separate_1_bdv "bdv / b = (1 / b) * bdv"
1.402 - separate_1_bdv_n "bdv ^^^ n / b = (1 / b) * bdv ^^^ n"
1.403 -
1.404 -end
1.405 -
1.406 -
1.407 -
1.408 -
1.409 -
1.410 -