
diff -r a28b5fc129b7 -r 22235e4dbe5f src/Tools/isac/Knowledge/PolyEq.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/isac/Knowledge/PolyEq.thy	Wed Aug 25 16:20:07 2010 +0200
@@ -0,0 +1,407 @@
+(*.(c) by Richard Lang, 2003 .*)
+(* theory collecting all knowledge 
+   (predicates 'is_rootEq_in', 'is_sqrt_in', 'is_ratEq_in')
+   for PolynomialEquations.
+   alternative dependencies see Isac.thy
+   created by: rlang 
+         date: 02.07
+   changed by: rlang
+   last change by: rlang
+             date: 03.06.03
+*)
+
+(* remove_thy"PolyEq";
+   use_thy"Knowledge/Isac";
+   use_thy"Knowledge/PolyEq";
+   
+   remove_thy"PolyEq";
+   use_thy"Isac";
+
+   use"ROOT.ML";
+   cd"knowledge";
+   *)
+
+PolyEq = LinEq + RootRatEq + 
+(*-------------------- consts ------------------------------------------------*)
+consts
+
+(*---------scripts--------------------------*)
+  Complete'_square
+             :: "[bool,real, \
+		  \ bool list] => bool list"
+               ("((Script Complete'_square (_ _ =))// \
+                 \ (_))" 9)
+ (*----- poly ----- *)	 
+  Normalize'_poly
+             :: "[bool,real, \
+		  \ bool list] => bool list"
+               ("((Script Normalize'_poly (_ _=))// \
+                 \ (_))" 9)
+  Solve'_d0'_polyeq'_equation
+             :: "[bool,real, \
+		  \ bool list] => bool list"
+               ("((Script Solve'_d0'_polyeq'_equation (_ _ =))// \
+                 \ (_))" 9)
+  Solve'_d1'_polyeq'_equation
+             :: "[bool,real, \
+		  \ bool list] => bool list"
+               ("((Script Solve'_d1'_polyeq'_equation (_ _ =))// \
+                 \ (_))" 9)
+  Solve'_d2'_polyeq'_equation
+             :: "[bool,real, \
+		  \ bool list] => bool list"
+               ("((Script Solve'_d2'_polyeq'_equation (_ _ =))// \
+                 \ (_))" 9)
+  Solve'_d2'_polyeq'_sqonly'_equation
+             :: "[bool,real, \
+		  \ bool list] => bool list"
+               ("((Script Solve'_d2'_polyeq'_sqonly'_equation (_ _ =))// \
+                 \ (_))" 9)
+  Solve'_d2'_polyeq'_bdvonly'_equation
+             :: "[bool,real, \
+		  \ bool list] => bool list"
+               ("((Script Solve'_d2'_polyeq'_bdvonly'_equation (_ _ =))// \
+                 \ (_))" 9)
+  Solve'_d2'_polyeq'_pq'_equation
+             :: "[bool,real, \
+		  \ bool list] => bool list"
+               ("((Script Solve'_d2'_polyeq'_pq'_equation (_ _ =))// \
+                 \ (_))" 9)
+  Solve'_d2'_polyeq'_abc'_equation
+             :: "[bool,real, \
+		  \ bool list] => bool list"
+               ("((Script Solve'_d2'_polyeq'_abc'_equation (_ _ =))// \
+                 \ (_))" 9)
+  Solve'_d3'_polyeq'_equation
+             :: "[bool,real, \
+		  \ bool list] => bool list"
+               ("((Script Solve'_d3'_polyeq'_equation (_ _ =))// \
+                 \ (_))" 9)
+  Solve'_d4'_polyeq'_equation
+             :: "[bool,real, \
+		  \ bool list] => bool list"
+               ("((Script Solve'_d4'_polyeq'_equation (_ _ =))// \
+                 \ (_))" 9)
+  Biquadrat'_poly
+             :: "[bool,real, \
+		  \ bool list] => bool list"
+               ("((Script Biquadrat'_poly (_ _=))// \
+                 \ (_))" 9)
+
+(*-------------------- rules -------------------------------------------------*)
+rules 
+
+  cancel_leading_coeff1 "Not (c =!= 0) ==> (a + b*bdv + c*bdv^^^2 = 0) = \
+			\                  (a/c + b/c*bdv + bdv^^^2 = 0)"
+  cancel_leading_coeff2 "Not (c =!= 0) ==> (a - b*bdv + c*bdv^^^2 = 0) = \
+			\                  (a/c - b/c*bdv + bdv^^^2 = 0)"
+  cancel_leading_coeff3 "Not (c =!= 0) ==> (a + b*bdv - c*bdv^^^2 = 0) = \
+			\                  (a/c + b/c*bdv - bdv^^^2 = 0)"
+
+  cancel_leading_coeff4 "Not (c =!= 0) ==> (a +   bdv + c*bdv^^^2 = 0) = \
+			\                  (a/c + 1/c*bdv + bdv^^^2 = 0)"
+  cancel_leading_coeff5 "Not (c =!= 0) ==> (a -   bdv + c*bdv^^^2 = 0) = \
+			\                  (a/c - 1/c*bdv + bdv^^^2 = 0)"
+  cancel_leading_coeff6 "Not (c =!= 0) ==> (a +   bdv - c*bdv^^^2 = 0) = \
+			\                  (a/c + 1/c*bdv - bdv^^^2 = 0)"
+
+  cancel_leading_coeff7 "Not (c =!= 0) ==> (    b*bdv + c*bdv^^^2 = 0) = \
+			\                  (    b/c*bdv + bdv^^^2 = 0)"
+  cancel_leading_coeff8 "Not (c =!= 0) ==> (    b*bdv - c*bdv^^^2 = 0) = \
+			\                  (    b/c*bdv - bdv^^^2 = 0)"
+
+  cancel_leading_coeff9 "Not (c =!= 0) ==> (      bdv + c*bdv^^^2 = 0) = \
+			\                  (      1/c*bdv + bdv^^^2 = 0)"
+  cancel_leading_coeff10"Not (c =!= 0) ==> (      bdv - c*bdv^^^2 = 0) = \
+			\                  (      1/c*bdv - bdv^^^2 = 0)"
+
+  cancel_leading_coeff11"Not (c =!= 0) ==> (a +      b*bdv^^^2 = 0) = \
+			\                  (a/b +      bdv^^^2 = 0)"
+  cancel_leading_coeff12"Not (c =!= 0) ==> (a -      b*bdv^^^2 = 0) = \
+			\                  (a/b -      bdv^^^2 = 0)"
+  cancel_leading_coeff13"Not (c =!= 0) ==> (         b*bdv^^^2 = 0) = \
+			\                  (           bdv^^^2 = 0/b)"
+
+  complete_square1      "(q + p*bdv + bdv^^^2 = 0) = \
+		        \(q + (p/2 + bdv)^^^2 = (p/2)^^^2)"
+  complete_square2      "(    p*bdv + bdv^^^2 = 0) = \
+		        \(    (p/2 + bdv)^^^2 = (p/2)^^^2)"
+  complete_square3      "(      bdv + bdv^^^2 = 0) = \
+		        \(    (1/2 + bdv)^^^2 = (1/2)^^^2)"
+		        
+  complete_square4      "(q - p*bdv + bdv^^^2 = 0) = \
+		        \(q + (p/2 - bdv)^^^2 = (p/2)^^^2)"
+  complete_square5      "(q + p*bdv - bdv^^^2 = 0) = \
+		        \(q + (p/2 - bdv)^^^2 = (p/2)^^^2)"
+
+  square_explicit1      "(a + b^^^2 = c) = ( b^^^2 = c - a)"
+  square_explicit2      "(a - b^^^2 = c) = (-(b^^^2) = c - a)"
+
+  bdv_explicit1         "(a + bdv = b) = (bdv = - a + b)"
+  bdv_explicit2         "(a - bdv = b) = ((-1)*bdv = - a + b)"
+  bdv_explicit3         "((-1)*bdv = b) = (bdv = (-1)*b)"
+
+  plus_leq              "(0 <= a + b) = ((-1)*b <= a)"(*Isa?*)
+  minus_leq             "(0 <= a - b) = (     b <= a)"(*Isa?*)
+
+(*-- normalize --*)
+  (*WN0509 compare LinEq.all_left "[|Not(b=!=0)|] ==> (a=b) = (a+(-1)*b=0)"*)
+  all_left
+    "[|Not(b=!=0)|] ==> (a = b) = (a - b = 0)"
+  makex1_x
+    "a^^^1  = a"  
+  real_assoc_1
+   "a+(b+c) = a+b+c"
+  real_assoc_2
+   "a*(b*c) = a*b*c"
+
+(* ---- degree 0 ----*)
+  d0_true
+  "(0=0) = True"
+  d0_false
+  "[|Not(bdv occurs_in a);Not(a=0)|] ==> (a=0) = False"
+(* ---- degree 1 ----*)
+  d1_isolate_add1
+   "[|Not(bdv occurs_in a)|] ==> (a + b*bdv = 0) = (b*bdv = (-1)*a)"
+  d1_isolate_add2
+   "[|Not(bdv occurs_in a)|] ==> (a +   bdv = 0) = (  bdv = (-1)*a)"
+  d1_isolate_div
+   "[|Not(b=0);Not(bdv occurs_in c)|] ==> (b*bdv = c) = (bdv = c/b)"
+(* ---- degree 2 ----*)
+  d2_isolate_add1
+   "[|Not(bdv occurs_in a)|] ==> (a + b*bdv^^^2=0) = (b*bdv^^^2= (-1)*a)"
+  d2_isolate_add2
+   "[|Not(bdv occurs_in a)|] ==> (a +   bdv^^^2=0) = (  bdv^^^2= (-1)*a)"
+  d2_isolate_div
+   "[|Not(b=0);Not(bdv occurs_in c)|] ==> (b*bdv^^^2=c) = (bdv^^^2=c/b)"
+  d2_prescind1
+   "(a*bdv + b*bdv^^^2 = 0) = (bdv*(a +b*bdv)=0)"
+  d2_prescind2
+   "(a*bdv +   bdv^^^2 = 0) = (bdv*(a +  bdv)=0)"
+  d2_prescind3
+   "(  bdv + b*bdv^^^2 = 0) = (bdv*(1+b*bdv)=0)"
+  d2_prescind4
+   "(  bdv +   bdv^^^2 = 0) = (bdv*(1+  bdv)=0)"
+  (* eliminate degree 2 *)
+  (* thm for neg arguments in sqroot have postfix _neg *)
+  d2_sqrt_equation1
+  "[|(0<=c);Not(bdv occurs_in c)|] ==> (bdv^^^2=c) = ((bdv=sqrt c) | (bdv=(-1)*sqrt c ))"
+  d2_sqrt_equation1_neg
+  "[|(c<0);Not(bdv occurs_in c)|] ==> (bdv^^^2=c) = False"
+  d2_sqrt_equation2
+  "(bdv^^^2=0) = (bdv=0)"
+  d2_sqrt_equation3
+  "(b*bdv^^^2=0) = (bdv=0)"
+  d2_reduce_equation1
+  "(bdv*(a +b*bdv)=0) = ((bdv=0)|(a+b*bdv=0))"
+  d2_reduce_equation2
+  "(bdv*(a +  bdv)=0) = ((bdv=0)|(a+  bdv=0))"
+  d2_pqformula1
+   "[|0<=p^^^2 - 4*q|] ==> (q+p*bdv+   bdv^^^2=0) =
+           ((bdv= (-1)*(p/2) + sqrt(p^^^2 - 4*q)/2) 
+          | (bdv= (-1)*(p/2) - sqrt(p^^^2 - 4*q)/2))"
+  d2_pqformula1_neg
+   "[|p^^^2 - 4*q<0|] ==> (q+p*bdv+   bdv^^^2=0) = False"
+  d2_pqformula2
+   "[|0<=p^^^2 - 4*q|] ==> (q+p*bdv+1*bdv^^^2=0) = 
+           ((bdv= (-1)*(p/2) + sqrt(p^^^2 - 4*q)/2) 
+          | (bdv= (-1)*(p/2) - sqrt(p^^^2 - 4*q)/2))"
+  d2_pqformula2_neg
+   "[|p^^^2 - 4*q<0|] ==> (q+p*bdv+1*bdv^^^2=0) = False"
+  d2_pqformula3
+   "[|0<=1 - 4*q|] ==> (q+  bdv+   bdv^^^2=0) = 
+           ((bdv= (-1)*(1/2) + sqrt(1 - 4*q)/2) 
+          | (bdv= (-1)*(1/2) - sqrt(1 - 4*q)/2))"
+  d2_pqformula3_neg
+   "[|1 - 4*q<0|] ==> (q+  bdv+   bdv^^^2=0) = False"
+  d2_pqformula4
+   "[|0<=1 - 4*q|] ==> (q+  bdv+1*bdv^^^2=0) = 
+           ((bdv= (-1)*(1/2) + sqrt(1 - 4*q)/2) 
+          | (bdv= (-1)*(1/2) - sqrt(1 - 4*q)/2))"
+  d2_pqformula4_neg
+   "[|1 - 4*q<0|] ==> (q+  bdv+1*bdv^^^2=0) = False"
+  d2_pqformula5
+   "[|0<=p^^^2 - 0|] ==> (  p*bdv+   bdv^^^2=0) =
+           ((bdv= (-1)*(p/2) + sqrt(p^^^2 - 0)/2) 
+          | (bdv= (-1)*(p/2) - sqrt(p^^^2 - 0)/2))"
+  (* d2_pqformula5_neg not need p^2 never less zero in R *)
+  d2_pqformula6
+   "[|0<=p^^^2 - 0|] ==> (  p*bdv+1*bdv^^^2=0) = 
+           ((bdv= (-1)*(p/2) + sqrt(p^^^2 - 0)/2) 
+          | (bdv= (-1)*(p/2) - sqrt(p^^^2 - 0)/2))"
+  (* d2_pqformula6_neg not need p^2 never less zero in R *)
+  d2_pqformula7
+   "[|0<=1 - 0|] ==> (    bdv+   bdv^^^2=0) = 
+           ((bdv= (-1)*(1/2) + sqrt(1 - 0)/2) 
+          | (bdv= (-1)*(1/2) - sqrt(1 - 0)/2))"
+  (* d2_pqformula7_neg not need, because 1<0 ==> False*)
+  d2_pqformula8
+   "[|0<=1 - 0|] ==> (    bdv+1*bdv^^^2=0) = 
+           ((bdv= (-1)*(1/2) + sqrt(1 - 0)/2) 
+          | (bdv= (-1)*(1/2) - sqrt(1 - 0)/2))"
+  (* d2_pqformula8_neg not need, because 1<0 ==> False*)
+  d2_pqformula9
+   "[|Not(bdv occurs_in q); 0<= (-1)*4*q|] ==> (q+    1*bdv^^^2=0) = 
+           ((bdv= 0 + sqrt(0 - 4*q)/2) 
+          | (bdv= 0 - sqrt(0 - 4*q)/2))"
+  d2_pqformula9_neg
+   "[|Not(bdv occurs_in q); (-1)*4*q<0|] ==> (q+    1*bdv^^^2=0) = False"
+  d2_pqformula10
+   "[|Not(bdv occurs_in q); 0<= (-1)*4*q|] ==> (q+     bdv^^^2=0) = 
+           ((bdv= 0 + sqrt(0 - 4*q)/2) 
+          | (bdv= 0 - sqrt(0 - 4*q)/2))"
+  d2_pqformula10_neg
+   "[|Not(bdv occurs_in q); (-1)*4*q<0|] ==> (q+     bdv^^^2=0) = False"
+  d2_abcformula1
+   "[|0<=b^^^2 - 4*a*c|] ==> (c + b*bdv+a*bdv^^^2=0) =
+           ((bdv=( -b + sqrt(b^^^2 - 4*a*c))/(2*a)) 
+          | (bdv=( -b - sqrt(b^^^2 - 4*a*c))/(2*a)))"
+  d2_abcformula1_neg
+   "[|b^^^2 - 4*a*c<0|] ==> (c + b*bdv+a*bdv^^^2=0) = False"
+  d2_abcformula2
+   "[|0<=1 - 4*a*c|]     ==> (c+    bdv+a*bdv^^^2=0) = 
+           ((bdv=( -1 + sqrt(1 - 4*a*c))/(2*a)) 
+          | (bdv=( -1 - sqrt(1 - 4*a*c))/(2*a)))"
+  d2_abcformula2_neg
+   "[|1 - 4*a*c<0|]     ==> (c+    bdv+a*bdv^^^2=0) = False"
+  d2_abcformula3
+   "[|0<=b^^^2 - 4*1*c|] ==> (c + b*bdv+  bdv^^^2=0) =
+           ((bdv=( -b + sqrt(b^^^2 - 4*1*c))/(2*1)) 
+          | (bdv=( -b - sqrt(b^^^2 - 4*1*c))/(2*1)))"
+  d2_abcformula3_neg
+   "[|b^^^2 - 4*1*c<0|] ==> (c + b*bdv+  bdv^^^2=0) = False"
+  d2_abcformula4
+   "[|0<=1 - 4*1*c|] ==> (c +   bdv+  bdv^^^2=0) =
+           ((bdv=( -1 + sqrt(1 - 4*1*c))/(2*1)) 
+          | (bdv=( -1 - sqrt(1 - 4*1*c))/(2*1)))"
+  d2_abcformula4_neg
+   "[|1 - 4*1*c<0|] ==> (c +   bdv+  bdv^^^2=0) = False"
+  d2_abcformula5
+   "[|Not(bdv occurs_in c); 0<=0 - 4*a*c|] ==> (c +  a*bdv^^^2=0) =
+           ((bdv=( 0 + sqrt(0 - 4*a*c))/(2*a)) 
+          | (bdv=( 0 - sqrt(0 - 4*a*c))/(2*a)))"
+  d2_abcformula5_neg
+   "[|Not(bdv occurs_in c); 0 - 4*a*c<0|] ==> (c +  a*bdv^^^2=0) = False"
+  d2_abcformula6
+   "[|Not(bdv occurs_in c); 0<=0 - 4*1*c|]     ==> (c+    bdv^^^2=0) = 
+           ((bdv=( 0 + sqrt(0 - 4*1*c))/(2*1)) 
+          | (bdv=( 0 - sqrt(0 - 4*1*c))/(2*1)))"
+  d2_abcformula6_neg
+   "[|Not(bdv occurs_in c); 0 - 4*1*c<0|]     ==> (c+    bdv^^^2=0) = False"
+  d2_abcformula7
+   "[|0<=b^^^2 - 0|]     ==> (    b*bdv+a*bdv^^^2=0) = 
+           ((bdv=( -b + sqrt(b^^^2 - 0))/(2*a)) 
+          | (bdv=( -b - sqrt(b^^^2 - 0))/(2*a)))"
+  (* d2_abcformula7_neg not need b^2 never less zero in R *)
+  d2_abcformula8
+   "[|0<=b^^^2 - 0|] ==> (    b*bdv+  bdv^^^2=0) =
+           ((bdv=( -b + sqrt(b^^^2 - 0))/(2*1)) 
+          | (bdv=( -b - sqrt(b^^^2 - 0))/(2*1)))"
+  (* d2_abcformula8_neg not need b^2 never less zero in R *)
+  d2_abcformula9
+   "[|0<=1 - 0|]     ==> (      bdv+a*bdv^^^2=0) = 
+           ((bdv=( -1 + sqrt(1 - 0))/(2*a)) 
+          | (bdv=( -1 - sqrt(1 - 0))/(2*a)))"
+  (* d2_abcformula9_neg not need, because 1<0 ==> False*)
+  d2_abcformula10
+   "[|0<=1 - 0|] ==> (      bdv+  bdv^^^2=0) =
+           ((bdv=( -1 + sqrt(1 - 0))/(2*1)) 
+          | (bdv=( -1 - sqrt(1 - 0))/(2*1)))"
+  (* d2_abcformula10_neg not need, because 1<0 ==> False*)
+
+(* ---- degree 3 ----*)
+  d3_reduce_equation1
+  "(a*bdv + b*bdv^^^2 + c*bdv^^^3=0) = (bdv=0 | (a + b*bdv + c*bdv^^^2=0))"
+  d3_reduce_equation2
+  "(  bdv + b*bdv^^^2 + c*bdv^^^3=0) = (bdv=0 | (1 + b*bdv + c*bdv^^^2=0))"
+  d3_reduce_equation3
+  "(a*bdv +   bdv^^^2 + c*bdv^^^3=0) = (bdv=0 | (a +   bdv + c*bdv^^^2=0))"
+  d3_reduce_equation4
+  "(  bdv +   bdv^^^2 + c*bdv^^^3=0) = (bdv=0 | (1 +   bdv + c*bdv^^^2=0))"
+  d3_reduce_equation5
+  "(a*bdv + b*bdv^^^2 +   bdv^^^3=0) = (bdv=0 | (a + b*bdv +   bdv^^^2=0))"
+  d3_reduce_equation6
+  "(  bdv + b*bdv^^^2 +   bdv^^^3=0) = (bdv=0 | (1 + b*bdv +   bdv^^^2=0))"
+  d3_reduce_equation7
+  "(a*bdv +   bdv^^^2 +   bdv^^^3=0) = (bdv=0 | (1 +   bdv +   bdv^^^2=0))"
+  d3_reduce_equation8
+  "(  bdv +   bdv^^^2 +   bdv^^^3=0) = (bdv=0 | (1 +   bdv +   bdv^^^2=0))"
+  d3_reduce_equation9
+  "(a*bdv             + c*bdv^^^3=0) = (bdv=0 | (a         + c*bdv^^^2=0))"
+  d3_reduce_equation10
+  "(  bdv             + c*bdv^^^3=0) = (bdv=0 | (1         + c*bdv^^^2=0))"
+  d3_reduce_equation11
+  "(a*bdv             +   bdv^^^3=0) = (bdv=0 | (a         +   bdv^^^2=0))"
+  d3_reduce_equation12
+  "(  bdv             +   bdv^^^3=0) = (bdv=0 | (1         +   bdv^^^2=0))"
+  d3_reduce_equation13
+  "(        b*bdv^^^2 + c*bdv^^^3=0) = (bdv=0 | (    b*bdv + c*bdv^^^2=0))"
+  d3_reduce_equation14
+  "(          bdv^^^2 + c*bdv^^^3=0) = (bdv=0 | (      bdv + c*bdv^^^2=0))"
+  d3_reduce_equation15
+  "(        b*bdv^^^2 +   bdv^^^3=0) = (bdv=0 | (    b*bdv +   bdv^^^2=0))"
+  d3_reduce_equation16
+  "(          bdv^^^2 +   bdv^^^3=0) = (bdv=0 | (      bdv +   bdv^^^2=0))"
+  d3_isolate_add1
+  "[|Not(bdv occurs_in a)|] ==> (a + b*bdv^^^3=0) = (b*bdv^^^3= (-1)*a)"
+  d3_isolate_add2
+  "[|Not(bdv occurs_in a)|] ==> (a +   bdv^^^3=0) = (  bdv^^^3= (-1)*a)"
+  d3_isolate_div
+   "[|Not(b=0);Not(bdv occurs_in a)|] ==> (b*bdv^^^3=c) = (bdv^^^3=c/b)"
+  d3_root_equation2
+  "(bdv^^^3=0) = (bdv=0)"
+  d3_root_equation1
+  "(bdv^^^3=c) = (bdv = nroot 3 c)"
+
+(* ---- degree 4 ----*)
+ (* RL03.FIXME es wir nicht getestet ob u>0 *)
+ d4_sub_u1
+ "(c+b*bdv^^^2+a*bdv^^^4=0) =
+   ((a*u^^^2+b*u+c=0) & (bdv^^^2=u))"
+
+(* ---- 7.3.02 von Termorder ---- *)
+
+  bdv_collect_1       "l * bdv + m * bdv = (l + m) * bdv"
+  bdv_collect_2       "bdv + m * bdv = (1 + m) * bdv"
+  bdv_collect_3       "l * bdv + bdv = (l + 1) * bdv"
+
+(*  bdv_collect_assoc0_1 "l * bdv + m * bdv + k = (l + m) * bdv + k"
+    bdv_collect_assoc0_2 "bdv + m * bdv + k = (1 + m) * bdv + k"
+    bdv_collect_assoc0_3 "l * bdv + bdv + k = (l + 1) * bdv + k"
+*)
+  bdv_collect_assoc1_1 "l * bdv + (m * bdv + k) = (l + m) * bdv + k"
+  bdv_collect_assoc1_2 "bdv + (m * bdv + k) = (1 + m) * bdv + k"
+  bdv_collect_assoc1_3 "l * bdv + (bdv + k) = (l + 1) * bdv + k"
+
+  bdv_collect_assoc2_1 "k + l * bdv + m * bdv = k + (l + m) * bdv"
+  bdv_collect_assoc2_2 "k + bdv + m * bdv = k + (1 + m) * bdv"
+  bdv_collect_assoc2_3 "k + l * bdv + bdv = k + (l + 1) * bdv"
+
+
+  bdv_n_collect_1      "l * bdv^^^n + m * bdv^^^n = (l + m) * bdv^^^n"
+  bdv_n_collect_2      " bdv^^^n + m * bdv^^^n = (1 + m) * bdv^^^n"
+  bdv_n_collect_3      "l * bdv^^^n + bdv^^^n = (l + 1) * bdv^^^n"   (*order!*)
+
+  bdv_n_collect_assoc1_1 "l * bdv^^^n + (m * bdv^^^n + k) = (l + m) * bdv^^^n + k"
+  bdv_n_collect_assoc1_2 "bdv^^^n + (m * bdv^^^n + k) = (1 + m) * bdv^^^n + k"
+  bdv_n_collect_assoc1_3 "l * bdv^^^n + (bdv^^^n + k) = (l + 1) * bdv^^^n + k"
+
+  bdv_n_collect_assoc2_1 "k + l * bdv^^^n + m * bdv^^^n = k + (l + m) * bdv^^^n"
+  bdv_n_collect_assoc2_2 "k + bdv^^^n + m * bdv^^^n = k + (1 + m) * bdv^^^n"
+  bdv_n_collect_assoc2_3 "k + l * bdv^^^n + bdv^^^n = k + (l + 1) * bdv^^^n"
+
+(*WN.14.3.03*)
+  real_minus_div         "- (a / b) = (-1 * a) / b"
+
+  separate_bdv           "(a * bdv) / b = (a / b) * bdv"
+  separate_bdv_n         "(a * bdv ^^^ n) / b = (a / b) * bdv ^^^ n"
+  separate_1_bdv         "bdv / b = (1 / b) * bdv"
+  separate_1_bdv_n       "bdv ^^^ n / b = (1 / b) * bdv ^^^ n"
+
+end
+
+
+
+
+
+




