"-------- WN1309xx non-terminating rls norm_Rational -------------------------";

 "-------- WN1309xx non-terminating rls norm_Rational -------------------------";

 "-------- WN1309xx non-terminating rls norm_Rational -------------------------";

 (*------- Schalk I, p.70 Nr. 480b; a/b : c/d translated to a/b * d/c*)

 val t = str2term 

   ("((12*x*y / (9*x^^^2 - y^^^2))  /  (1 / (3*x - y)^^^2 - 1 / (3*x + y)^^^2))  *  " ^

 	"((1/(x - 5*y)^^^2  -  1/(x + 5*y)^^^2)  /  (20*x*y / (x^^^2 - 25*y^^^2)))");

 (*1st factor separately simplified *)

 val t = str2term "((12*x*y / (9*x^^^2 - y^^^2))  /  (1 / (3*x - y)^^^2 - 1 / (3*x + y)^^^2))";

 val SOME (t', _) = rewrite_set_ thy false norm_Rational t; 

 if term2str t' = "(-9 * x ^^^ 2 + y ^^^ 2) / -1" then () else error "Nr. 480b lhs changed";

 (*2nd factor separately simplified *)

 val t = str2term "((1/(x - 5*y)^^^2  -  1/(x + 5*y)^^^2)  /  (20*x*y / (x^^^2 - 25*y^^^2)))";

 val SOME (t',_) = rewrite_set_ thy false norm_Rational t; term2str t';

 if term2str t' = "-1 / (-1 * x ^^^ 2 + 25 * y ^^^ 2)" then () else error "Nr. 480b rhs changed";

 "-------- Schalk I, p.70 Nr. 477a: terms are exploding ?!?";

 val t = str2term ("b*y/(b - 2*y)/((b^^^2 - y^^^2)/(b+2*y))  /" ^

 		 "(b^^^2*y + b*y^^^2) * (a+x)^^^2  /  ((b^^^2 - 4*y^^^2) * (a+2*x)^^^2)");

 (*val SOME (t',_) = rewrite_set_ thy false norm_Rational t;

 :

 ###  rls: cancel_p on: (a ^^^ 2 * (b * y) + 2 * (a * (b * (x * y))) + b * (x ^^^ 2 * y)) /

 (b + -2 * y) /

 ((b ^^^ 2 + -1 * y ^^^ 2) / (b + 2 * y)) /

 (b ^^^ 2 * y + b * y ^^^ 2) /

 (a ^^^ 2 * b ^^^ 2 + -4 * (a ^^^ 2 * y ^^^ 2) + 4 * (a * (b ^^^ 2 * x)) +

  -16 * (a * (x * y ^^^ 2)) +

  4 * (b ^^^ 2 * x ^^^ 2) +

  -16 * (x ^^^ 2 * y ^^^ 2)) 

 exception Div raised

 BUT

 val t = str2term 

   ("(a ^^^ 2 * (b * y) + 2 * (a * (b * (x * y))) + b * (x ^^^ 2 * y)) /" ^

   "(b + -2 * y) /" ^

   "((b ^^^ 2 + -1 * y ^^^ 2) / (b + 2 * y)) /" ^

   "(b ^^^ 2 * y + b * y ^^^ 2) /" ^

   "(a ^^^ 2 * b ^^^ 2 + -4 * (a ^^^ 2 * y ^^^ 2) + 4 * (a * (b ^^^ 2 * x)) +" ^

   "-16 * (a * (x * y ^^^ 2)) +" ^

   "4 * (b ^^^ 2 * x ^^^ 2) +" ^

   "-16 * (x ^^^ 2 * y ^^^ 2))");

 NONE = cancel_p_ thy t;

 *)

 (*------- Schalk I, p.70 Nr. 476b in 2003 this worked using 10 sec. *)

 val t = str2term 

   ("((a^^^2 - b^^^2)/(2*a*b) + 2*a*b/(a^^^2 - b^^^2))  /  ((a^^^2 + b^^^2)/(2*a*b) + 1)    / " ^

    "((a^^^2 + b^^^2)^^^2  /  (a + b)^^^2)");

 (*

 trace_rewrite := true;

 rewrite_set_ thy false norm_Rational t;

 :

 ####  rls: cancel_p on: (2 * (a ^^^ 7 * b) + 4 * (a ^^^ 6 * b ^^^ 2) + 6 * (a ^^^ 5 * b ^^^ 3) +

  8 * (a ^^^ 4 * b ^^^ 4) +

  6 * (a ^^^ 3 * b ^^^ 5) +

  4 * (a ^^^ 2 * b ^^^ 6) +

  2 * (a * b ^^^ 7)) /

 (2 * (a ^^^ 9 * b) + 4 * (a ^^^ 8 * b ^^^ 2) +

  2 * (2 * (a ^^^ 7 * b ^^^ 3)) +

  4 * (a ^^^ 6 * b ^^^ 4) +

  -4 * (a ^^^ 4 * b ^^^ 6) +

  -4 * (a ^^^ 3 * b ^^^ 7) +

  -4 * (a ^^^ 2 * b ^^^ 8) +

  -2 * (a * b ^^^ 9))

 if term2str t = "1 / (a ^^^ 2 + -1 * b ^^^ 2)" then ()

 else error "rational.sml: diff.behav. in norm_Rational_mg 49";

 *)

 "-------- Schalk I, p.70 Nr. 480a: terms are exploding ?!?";

 val t = str2term ("(1/x + 1/y + 1/z)  /  (1/x - 1/y - 1/z)  /  " ^

   "(2*x^^^2 / (x^^^2 - z^^^2) / (x / (x + z)  +  x / (x - z)))");

 (*

 trace_rewrite := true;

 rewrite_set_ thy false norm_Rational t;

 :

 ####  rls: cancel_p on: (2 * (x ^^^ 6 * (y ^^^ 2 * z)) + 2 * (x ^^^ 6 * (y * z ^^^ 2)) +

  2 * (x ^^^ 5 * (y ^^^ 2 * z ^^^ 2)) +

  -2 * (x ^^^ 4 * (y ^^^ 2 * z ^^^ 3)) +

  -2 * (x ^^^ 4 * (y * z ^^^ 4)) +

  -2 * (x ^^^ 3 * (y ^^^ 2 * z ^^^ 4))) /

 (-2 * (x ^^^ 6 * (y ^^^ 2 * z)) + -2 * (x ^^^ 6 * (y * z ^^^ 2)) +

  2 * (x ^^^ 5 * (y ^^^ 2 * z ^^^ 2)) +

  2 * (x ^^^ 4 * (y ^^^ 2 * z ^^^ 3)) +

  2 * (x ^^^ 4 * (y * z ^^^ 4)) +

  -2 * (x ^^^ 3 * (y ^^^ 2 * z ^^^ 4)))

 *)

 "-------- Schalk I, p.60 Nr. 215d: terms are exploding, internal loop does not terminate";

 val t = str2term "(a-b)^^^3 * (x+y)^^^4 / ((x+y)^^^2 * (a-b)^^^5)";

 (* Kein Wunder, denn Z???ler und Nenner extra als Polynom dargestellt ergibt:

 val t = str2term "(a-b)^^^3 * (x+y)^^^4";

 val SOME (t, _) = rewrite_set_ thy false norm_Rational t;

 term2str t;

 "a^^^3 * x^^^4 + 4 * a^^^3 * x^^^3 * y +6 * a^^^3 * x^^^2 * y^^^2 +4 * a^^^3 * x * y^^^3 +a^^^3 * y^^^4 +-3 * a^^^2 * b * x^^^4 +-12 * a^^^2 * b * x^^^3 * y +-18 * a^^^2 * b * x^^^2 * y^^^2 +-12 * a^^^2 * b * x * y^^^3 +-3 * a^^^2 * b * y^^^4 +3 * a * b^^^2 * x^^^4 +12 * a * b^^^2 * x^^^3 * y +18 * a * b^^^2 * x^^^2 * y^^^2 +12 * a * b^^^2 * x * y^^^3 +3 * a * b^^^2 * y^^^4 +-1 * b^^^3 * x^^^4 +-4 * b^^^3 * x^^^3 * y +-6 * b^^^3 * x^^^2 * y^^^2 +-4 * b^^^3 * x * y^^^3 +-1 * b^^^3 * y^^^4";

 val t = str2term "((x+y)^^^2 * (a-b)^^^5)";

 val SOME (t, _) = rewrite_set_ thy false norm_Rational t;

 term2str t;

 "a^^^5 * x^^^2 + 2 * a^^^5 * x * y + a^^^5 * y^^^2 +-5 * a^^^4 * b * x^^^2 +-10 * a^^^4 * b * x * y +-5 * a^^^4 * b * y^^^2 +10 * a^^^3 * b^^^2 * x^^^2 +20 * a^^^3 * b^^^2 * x * y +10 * a^^^3 * b^^^2 * y^^^2 +-10 * a^^^2 * b^^^3 * x^^^2 +-20 * a^^^2 * b^^^3 * x * y +-10 * a^^^2 * b^^^3 * y^^^2 +5 * a * b^^^4 * x^^^2 +10 * a * b^^^4 * x * y +5 * a * b^^^4 * y^^^2 +-1 * b^^^5 * x^^^2 +-2 * b^^^5 * x * y +-1 * b^^^5 * y^^^2";

 anscheinend macht dem Rechner das Krzen diese Bruches keinen Spass mehr ...*)

 "-------- Schalk I, p.70 Nr. 480b: terms are exploding, trace_rewrite stops at";

 val t = str2term ("((12*x*y/(9*x^^^2 - y^^^2))/" ^

 		 "(1/(3*x - y)^^^2 - 1/(3*x + y)^^^2)) *" ^

 		 "(1/(x - 5*y)^^^2 - 1/(x + 5*y)^^^2)/" ^

 		 "(20*x*y/(x^^^2 - 25*y^^^2))");

 (*val SOME (t, _) = rewrite_set_ thy false norm_Rational t;

 :

 ####  rls: cancel_p on: (19440 * (x ^^^ 8 * y ^^^ 2) + -490320 * (x ^^^ 6 * y ^^^ 4) +

  108240 * (x ^^^ 4 * y ^^^ 6) +

  -6000 * (x ^^^ 2 * y ^^^ 8)) /

 (2160 * (x ^^^ 8 * y ^^^ 2) + -108240 * (x ^^^ 6 * y ^^^ 4) +

  1362000 * (x ^^^ 4 * y ^^^ 6) +

  -150000 * (x ^^^ 2 * y ^^^ 8))

 *)