(* tests for various kinds of univariate equations.

   Author: Richard Lang 2003

   (c) due to copyright terms

 These tests have not been updated with the transition Isabelle2002 --> 2011

 # because there are many other tests on equations in other test-files

 # some of these equations are twice, e.g. x / (x ^ 2 - 6 * x + 9) - 1 / (x ^ 2 - 3 * x) = 1 / x, x

 # this file needs specifically much cleaning.

 *)

 (******************************************************************

 WN.060104 transfer marked (*E..*)examples to the exp-collection

  # exp_IsacCore_Equ_Uni_Poly.xml   from rlang.sml    (*EP*)   exp

  # exp_IsacCore_Equ_Uni_Rat.xml    from rlang.sml    (*ER*)   exp

  # exp_IsacCore_Equ_Uni_Root.xml   from rlang.sml    (*EO*)   exp

 *******************************************************************)

 (*WN.12.6.03: for TODOs search 'writeln', for simplification search MG*)

 (* use"kbtest/rlang.sml";

    use"rlang.sml";

    (c) Richard Lang 2003

    tests over all equations implemented in his diploma thesis

    Elementare Gleichungen der Mittelschulmathematik in der ISAC Wissensbasis,

    Master's thesis, University of Technology, Graz, Austria, March 2003.

    created: 030228

    by: rlang

    last change: 030603

 *)

 (*@Book{bSchalk1,

   author =       {Schalk, Heinz-Christian and Binder, Christian and Fertl, Walter and 

                   Firneis, Friedrich and Gems, Werner and Lehner, Dieter and 

                   Plihal, Andreas and Würl,Manfred},

   title =        {Mathematik für höhere technische Lehranstalten Band I},

   publisher =    {Reniets Verlag},

   year =         {1986},

   note =         {Schulbuch-Nr. 942},

 }

 @Book{bSchalk2,

   author =       {Schalk, Heinz-Christian and Baumgartner, Gerhard and Binder, Christian and 

                   Eder, Hans Gerhard and Fertl, Walter and Firneis, Friedrich and 

                   Konstantiniuk, Peter and Plihal, Andreas and Rümmele, Goswin and 

                   Steinwender, Andreas and Zangerl, Nikolaus},

   title =        {Mathematik für höhere technische Lehranstalten Band II},

   publisher =    {Reniets Verlag},

   year =         {1987},

   note =         {Schulbuch-Nr. 1682},

 }

 *)

 (* Compiler.Control.Print.printDepth:=5; (*4 default*) 

 trace_rewrite:=true;

  trace_rewrite:=false;

  refine fmz ["univariate","equation"];

 *)

 "---- rlang.sml begin-----------------------------------";

 (*-----------------  Schalk I s.86 Bsp 5 ------------------------*)

 "Schalk I s.86 Bsp 5 (3*x - 1 - (5*x - (2 - 4*x)) = -11)";

 "Schalk I s.86 Bsp 5 (3*x - 1 - (5*x - (2 - 4*x)) = -11)";

 "Schalk I s.86 Bsp 5 (3*x - 1 - (5*x - (2 - 4*x)) = -11)";

 (*EP*)

 val fmz = ["equality (3*x - 1 - (5*x - (2 - 4*x)) = -11)",

 	   "solveFor x","solutions L"];

 val (dI',pI',mI') = ("PolyEq",["univariate","equation"],["no_met"]);

 (*val p = e_pos'; 

 val c = []; 

 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));

 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)

 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 2]")) => ()

 	 | _ => error "rlang.sml: diff.behav. in Schalk I s.86 Bsp 5 [x = 2]";

 (*-----------------  Schalk I s.86 Bsp 19 ------------------------*)

 "Schalk I s.86 Bsp 19 (x - 5)*(10 - x) = (3 - x)*(2 + x) + 2*(x + 20)";

 "Schalk I s.86 Bsp 19 (x - 5)*(10 - x) = (3 - x)*(2 + x) + 2*(x + 20)";

 "Schalk I s.86 Bsp 19 (x - 5)*(10 - x) = (3 - x)*(2 + x) + 2*(x + 20)";

 (*EP*)

 val fmz = ["equality ((x - 5)*(10 - x) = (3 - x)*(2 + x) + 2*(x + 20))",

 	   "solveFor x","solutions L"];

 val (dI',pI',mI') = ("PolyEq",["univariate","equation"],["no_met"]);

 (*val p = e_pos'; 

 val c = []; 

 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));

 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)

 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 8]")) => ()

 	 | _ => error "rlang.sml: diff.behav. in Schalk I s.86 Bsp 19 [x = 8]";

 (*-----------------  Schalk I s.86 Bsp 23 ------------------------*)

 "Schalk I s.86 Bsp 19 ((2*x+5)^^^2+(3*x+4)^^^2=(13*x+2)*(x+1)+2*(15+14*x))";

 "Schalk I s.86 Bsp 19 ((2*x+5)^^^2+(3*x+4)^^^2=(13*x+2)*(x+1)+2*(15+14*x))";

 "Schalk I s.86 Bsp 19 ((2*x+5)^^^2+(3*x+4)^^^2=(13*x+2)*(x+1)+2*(15+14*x))";

 (*EP*)

 val fmz = ["equality ((2*x+5)^^^2+(3*x+4)^^^2=(13*x+2)*(x+1)+2*(15+14*x))",

 	   "solveFor x","solutions L"];

 val (dI',pI',mI') = ("PolyEq",["univariate","equation"],["no_met"]);

 (*val p = e_pos'; 

 val c = []; 

 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));

 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)

 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = -9]")) => ()

 	 | _ => error "rlang.sml: diff.behav. in Schalk I s.86 Bsp 23 [x = -9]";

 (*-----------------  Schalk I s.86 Bsp 25 ------------------------*)

 "Schalk I s.86 Bsp 25 ((2*x+1)^^^3+(x+1)^^^3=(2*x+1)^^^2*2*x+(x+2)^^^3+x^^^2)";

 "Schalk I s.86 Bsp 25 ((2*x+1)^^^3+(x+1)^^^3=(2*x+1)^^^2*2*x+(x+2)^^^3+x^^^2)";

 "Schalk I s.86 Bsp 25 ((2*x+1)^^^3+(x+1)^^^3=(2*x+1)^^^2*2*x+(x+2)^^^3+x^^^2)";

 (*EP*)

 val fmz = ["equality ((2*x+1)^^^3+(x+1)^^^3=(2*x+1)^^^2*2*x+(x+2)^^^3+x^^^2)",

 	   "solveFor x","solutions L"];

 val (dI',pI',mI') = ("PolyEq",["univariate","equation"],["no_met"]);

 (*val p = e_pos'; 

 val c = []; 

 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));

 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)

 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = -6 / 5]")) => ()

 	 | _ => error "rlang.sml: diff.behav. in Schalk I s.86 Bsp 25 [x = -6 / 5]";

 (*-----------------  Schalk I s.86 Bsp 28b ------------------------*)

 "Schalk I s.86 Bsp 28b ((3*x+5)/18 - x/2 = -((3*x - 2)/9))";

 "Schalk I s.86 Bsp 28b ((3*x+5)/18 - x/2 = -((3*x - 2)/9))";

 "Schalk I s.86 Bsp 28b ((3*x+5)/18 - x/2 = -((3*x - 2)/9))";

 (*ER-2*)

 val fmz = ["equality ((3*x+5)/18 - x/2 = -((3*x - 2)/9))",

 	   "solveFor x","solutions L"];

 val (dI',pI',mI') = ("PolyEq",["univariate","equation"],["no_met"]);

 (*val p = e_pos'; val c = []; 

 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));

 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)

 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; f2str f;

 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[]")) => ()

 	 | _ => error "rlang.sml: diff.behav. in Schalk I s.86 Bsp 28b []";

 (*WN---v *)

 val bdv= (term_of o the o (parse thy)) "bdv";

 val v = (term_of o the o (parse thy)) "x";

 val t = (term_of o the o (parse thy)) "3 * x / 5";

 val SOME (t',_) = rewrite_set_inst_ PolyEq.thy true 

 				    [(bdv, v)] make_ratpoly_in t;

 if term2str t' = "3 / 5 * x" then () else error "rlang.sml: 1";

 val t = str2term "(3*x+5)/18 - x/2  - -(3*x - 2)/9 = 0";

 val subst = [(str2term "bdv", str2term "x")];

 val SOME (t',_) = rewrite_set_inst_ thy false subst make_ratpoly_in t;

 if term2str t' = "1 / 18 = 0" then () else error "rlang.sml: 2";

 (*WN---^ *)

 (*-----------------  Schalk I s.87 Bsp 36b ------------------------*)

 "Schalk I s.87 Bsp 36b ((17*x - 51)/9 - (-(13*x - 3)/6) + 11 -(9*x- 7)/4 = 0)";

 "Schalk I s.87 Bsp 36b ((17*x - 51)/9 - (-(13*x - 3)/6) + 11 -(9*x- 7)/4 = 0)";

 "Schalk I s.87 Bsp 36b ((17*x - 51)/9 - (-(13*x - 3)/6) + 11 -(9*x- 7)/4 = 0)";

 (*ER-1*)

 val fmz = ["equality ((17*x - 51)/9 - (-(13*x - 3)/6) + 11 - (9*x - 7)/4 = 0)",

 	   "solveFor x","solutions L"];

 val (dI',pI',mI') = ("PolyEq",["univariate","equation"],["no_met"]);

 (*val p = e_pos'; 

 val c = []; 

 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));

 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)

 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = -237 / 65]")) => ()

 	 | _ => error "rlang.sml: diff.behav. in Schalk I s.86 Bsp 36b [x = -237 / 65]";

 (*WN---v *)

 val t = str2term "(17*x - 51)/9 - (-(13*x - 3)/6) + 11 - (9*x - 7)/4 = 0";

 val subst = [(str2term "bdv", str2term "x")];

 val SOME (t',_) = rewrite_set_inst_ thy false subst make_ratpoly_in t;

 term2str t';

 if term2str t' = "79 / 12 + 65 / 36 * x = 0" then () 

 else error "rlang.sml: 3";

 (*WN---^ *)

 (*-----------------  Schalk I s.87 Bsp 38b ------------------------*)

 "Schalk I s.87 Bsp 38b (-(2/x) + 3/(2*x) - 4/(3*x) + 5/(4*x) + 6/(5*x) =65/8)";

 "Schalk I s.87 Bsp 38b (-(2/x) + 3/(2*x) - 4/(3*x) + 5/(4*x) + 6/(5*x) =65/8)";

 "Schalk I s.87 Bsp 38b (-(2/x) + 3/(2*x) - 4/(3*x) + 5/(4*x) + 6/(5*x) =65/8)";

 (*ER-3*)

 val fmz = ["equality (-2/x + 3/(2*x) - 4/(3*x) + 5/(4*x) + 6/(5*x) = 65/8)",

 	   "solveFor x","solutions L"];

 val (dI',pI',mI') = ("RatEq",["univariate","equation"],["no_met"]);

 (*val p = e_pos'; 

 val c = []; 

 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));

 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)

 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 if f = Form' (FormKF (~1, EdUndef, 0, Nundef, "296 + -3900 * x = 0")) then ()

 else error "rlang.sml: diff.behav. in Schalk I s.87 Bsp 38b";

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 74 / 975]")) => ()

 	 | _ => error "rlang.sml: diff.behav. in Schalk I s.86 Bsp 38b [x = 74 / 975]";

 (*-----------------  Schalk I s.87 Bsp 40b ------------------------*)

 "Schalk I s.87 Bsp 40b ((x+3)/(2*x - 4)=3)";

 "Schalk I s.87 Bsp 40b ((x+3)/(2*x - 4)=3)";

 "Schalk I s.87 Bsp 40b ((x+3)/(2*x - 4)=3)";

 (*ER-4*)

 val fmz = ["equality ((x+3)/(2*x - 4)=3)",

 	   "solveFor x","solutions L"];

 val (dI',pI',mI') = ("RatEq",["univariate","equation"],["no_met"]);

 (*val p = e_pos'; 

 val c = []; 

 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));

 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)

 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; f2str f;

 (*val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;*)

 if f = Form' (FormKF (~1, EdUndef, 0, Nundef, "15 + -5 * x = 0")) then ()

 else error "rlang.sml: diff.behav. in Schalk I s.87 Bsp 40b";

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 3]")) => ()

 	 | _ => error "rlang.sml: diff.behav. in Schalk I s.87 Bsp 40b [x = 3]";

 (*-----------------  Schalk I s.87 Bsp 44a ------------------------*)

 "Schalk I s.87 Bsp 44a ((1/2+(5*x)/2)^^^2 -((13*x)/2- 5/2)^^^2 -(6*x)^^^2+29)";

 "Schalk I s.87 Bsp 44a ((1/2+(5*x)/2)^^^2 -((13*x)/2- 5/2)^^^2 -(6*x)^^^2+29)";

 "Schalk I s.87 Bsp 44a ((1/2+(5*x)/2)^^^2 -((13*x)/2- 5/2)^^^2 -(6*x)^^^2+29)";

 (*ER-5*)

 val fmz = ["equality ((1/2 + (5*x)/2)^^^2 - ((13*x)/2 - 5/2)^^^2 = -1*(6*x)^^^2 + 29)",

 	   "solveFor x","solutions L"];

 val (dI',pI',mI') = ("PolyEq",["univariate","equation"],["no_met"]);

 (*val p = e_pos'; 

 val c = []; 

 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));

 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)

 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];

 (*trace_rewrite:=true;

 *)

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 1]")) => ()

 	 | _ => error "rlang.sml: diff.behav. in Schalk I s.87 Bsp 44a [x = 1]";

 (*WN---v *)

 val t = str2term "(1/2 + (5*x)/2)^^^2 - ((13*x)/2 - 5/2)^^^2 - (6*x)^^^2 + 29";

 val subst = [(str2term "bdv", str2term "x")];

 val SOME (t',_) = rewrite_set_inst_ thy false subst make_ratpoly_in t;

 if term2str t' = "23 + 35 * x + -72 * x ^^^ 2" then () 

 else error "rlang.sml: 4";

 val t = str2term "(1/2 + (5*x)/2)^^^2 - ((13*x)/2 - 5/2)^^^2 + (6*x)^^^2 - 29";

 val subst = [(str2term "bdv", str2term "x")];

 val SOME (t',_) = rewrite_set_inst_ thy false subst make_ratpoly_in t;

 if term2str t' = "-35 + 35 * x" then () 

 else error "rlang.sml: 4.1";

 (*WN---^ *)

 (*-----------------  Schalk I s.87 Bsp 52a ------------------------*)

 "Schalk I s.87 Bsp 52a ((5*x)/(x - 2) - x/(x+2)=4)";

 "Schalk I s.87 Bsp 52a ((5*x)/(x - 2) - x/(x+2)=4)";

 "Schalk I s.87 Bsp 52a ((5*x)/(x - 2) - x/(x+2)=4)";

 (*ER-6*)

 val fmz = ["equality ((5*x)/(x - 2) - x/(x+2)=4)",

 	   "solveFor x","solutions L"];

 val (dI',pI',mI') = ("RatEq",["univariate","equation"],["no_met"]);

 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

  (*"12 * x + 4 * x ^^^ 2 = 4 * (-4 + x ^^^ 2)",Subproblem["normalize", "poly*)

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 if f = Form' (FormKF (~1, EdUndef, 0, Nundef, "16 + 12 * x = 0")) then ()

 else error "rlang.sml: diff.behav. in Schalk I s.87 Bsp 52a";

             (*Subproblem["degree_1", "polynomial", "univariate", "equation"]*)

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = -4 / 3]")) => ()

 	 | _ => error "rlang.sml: diff.behav. in  Schalk I s.87 Bsp 52a [x = -4 / 3]";

 (*-----------------  Schalk I s.88 Bsp 64c ------------------------*)

 "Schalk I s.88 Bsp 64c (((x - 1)/(x+1)+1)/((x - 1)/(x+1) - (x+1)/(x - 1))=2)";

 "Schalk I s.88 Bsp 64c (((x - 1)/(x+1)+1)/((x - 1)/(x+1) - (x+1)/(x - 1))=2)";

 "Schalk I s.88 Bsp 64c (((x - 1)/(x+1)+1)/((x - 1)/(x+1) - (x+1)/(x - 1))=2)";

 (*ER-8*)

 val fmz = ["equality (((x - 1)/(x+1)+1)/((x - 1)/(x+1) - (x+1)/(x - 1))=2)",

 	   "solveFor x","solutions L"];

 val (dI',pI',mI') = ("RatEq",["univariate","equation"],["no_met"]);

 (*val p = e_pos'; val c = []; 

 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));

 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)

 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; f2str f;

 if f = Form' (FormKF (~1, EdUndef, 0, Nundef, "-3 + -1 * x = 0")) then ()

 else error "rlangsml: diff.behav. in Schalk I s.88 Bsp 64c";

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 case f of Form' (FormKF (_,_,0,_,"[x = -3]")) => ()

 	 | _ => error "rlang.sml: diff.behav. in  Schalk I s.88 Bsp 64c [x = -3]";

 (*-----------------  Schalk I s.88 Bsp 79a (2) ------------------------*)

 "Schalk I s.88 Bsp 79a (2) (m1*v1+m2*v2=0)";

 "Schalk I s.88 Bsp 79a (2) (m1*v1+m2*v2=0)";

 "Schalk I s.88 Bsp 79a (2) (m1*v1+m2*v2=0)";

 (*ER-10*)

 val fmz = ["equality (m1*v1+m2*v2=0)",

 	   "solveFor m1","solutions L"];

 val (dI',pI',mI') = ("PolyEq",["univariate","equation"],["no_met"]);

 (*val p = e_pos'; val c = []; 

 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));

 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)

 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[m1 = -1 * m2 * v2 / v1]")) => ()

 	 | _ => error "rlang.sml: diff.behav. in  Schalk I s.88 Bsp 79a (2) [m1 = -1 * m2 * v2 / v1]";

 (*-----------------  Schalk I s.89 Bsp 90a(1) ------------------------*)

 "Schalk I s.89 Bsp 90a (1) (f=((w+u)/(w+v))*v0)";

 "Schalk I s.89 Bsp 90a (1) (f=((w+u)/(w+v))*v0)";

 "Schalk I s.89 Bsp 90a (1) (f=((w+u)/(w+v))*v0)";

 (*ER-11*)

 val fmz = ["equality (f=((w+u)/(w+v))*v0)",

 	   "solveFor v","solutions L"];

 val (dI',pI',mI') = ("RatEq",["univariate","equation"],["no_met"]);

 (*val p = e_pos'; val c = []; 

 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));

 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)

 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 (*val nxt = Specify_Problem ["rational","univariate","equation"])      *)

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 (*val nxt = Specify_Method ["RatEq","solve_rat_equation"])      *)

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 (*nxt = Subproblem ("RatEq",["univariate","equation"]))      *)

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 (*val nxt =Model_Problem ["normalize","polynomial","univariate","equation"])*)

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 (*val nxt = ("Apply_Method",Apply_Method ["PolyEq","normalize_poly"])*)

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 (*val nxt =Subproblem ("PolyEq",["polynomial","univariate","equation"]))*)

 if f = Form'

       (FormKF

          (~1,

             EdUndef,

             0,

             Nundef,

             "f * w + -1 * u * v0 + -1 * v0 * w + f * v = 0")) then ()

 else error "rlang.sml: diff.behav. in Schalk I s.89 Bsp 90a";

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 (*val nxt = Model_Problem ["degree_1","polynomial","univariate","equation"])*)

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 (*val nxt = ("Apply_Method",Apply_Method ["PolyEq","solve_d1_poly_equation"])*)

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 (*val f = "v = -1 * (f * w + -1 * u * v0 + -1 * v0 * w) / f")) : mout

 val nxt = ("Or_to_List",Or_to_List) : string * tac *)

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 (*val f = "[v = -1 * (f * w + -1 * u * v0 + -1 * v0 * w) / f]")) : mout

 val nxt = ("Check_elementwise",Check_elementwise "Assumptions") *)

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 (*val f = "[v = -1 * (f * w + -1 * u * v0 + -1 * v0 * w) / f]")) : mout

 val nxt = Check_Postcond ["degree_1","polynomial","univariate","equation"])*)

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 (*val f = "[v = -1 * (f * w + -1 * u * v0 + -1 * v0 * w) / f]")) : mout

 val nxt = Check_Postcond ["normalize","polynomial","univariate","equation"])*)

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 (*val f = "[v = -1 * (f * w + -1 * u * v0 + -1 * v0 * w) / f]")) : mout

 val nxt = ("Check_elementwise",Check_elementwise "Assumptions")*)

 get_assumptions_ pt p;

 (*it = ["v + w ~= 0"]    ... goes to the solution as an assumption*)

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 (*val f = Form' (FormKF (~1,EdUndef,1,Nundef,"[]")) : mout

 val nxt = Check_Postcond ["rational","univariate","equation"])        *)

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 case f of Form'  (FormKF (~1,EdUndef,0,Nundef,

         "[v = (u * v0 + v0 * w + -1 * f * w) / f]")) => ()

 	 | _ => error "rlang.sml: diff.behav. in  Schalk I s.89 Bsp 90a (1) [v=...]";

 if get_assumptions_ pt p = 

    [str2term"(u * v0 + v0 * w + -1 * f * w) / f + w ~= 0"] then () 

 else error "rlang.sml: diff.behav. in I s.89 Bsp 90a (1) [v=...] asm";

 (*-----------------  Schalk I s.89 Bsp 90a(2) ------------------------*)

 "Schalk I s.89 Bsp 90a (2) (f=((w+u)/(w+v))*v0)";

 "Schalk I s.89 Bsp 90a (2) (f=((w+u)/(w+v))*v0)";

 "Schalk I s.89 Bsp 90a (2) (f=((w+u)/(w+v))*v0)";

 (*ER-12*)

 val fmz = ["equality (f=((w+u)/(w+v))*v0)",

 	   "solveFor w","solutions L"];

 val (dI',pI',mI') = ("RatEq",["univariate","equation"],["no_met"]);

 (*val p = e_pos';val c = []; 

 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));

 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)

 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 if f = Form'

       (FormKF

          (~1,

             EdUndef,

             0,

             Nundef,

             "f * v + -1 * u * v0 + (f + -1 * v0) * w = 0")) then ()

 else error "rlang.sml: diff.behav. in Schalk I s.89 Bsp 90a (2)";

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[w = (u * v0 + -1 * f * v) / (f + -1 * v0)]")) => ()

 	 | _ => error "rlang.sml: diff.behav. in Schalk I Bsp 90a(2)";

 if get_assumptions_ pt p = 

 [str2term"v + (u * v0 + -1 * f * v) / (f + -1 * v0) ~= 0",

  str2term"f + -1 * v0 ~= 0"]

 then writeln "asm should be simplified ???" 

 else error "rlang.sml: diff.behav. in Schalk I Bsp 90a(2) asm";

 (*-----------------  Schalk I s.89 Bsp 98a(1) ------------------------*)

 "Schalk I s.89 Bsp 98a (1) (1/R=1/R1+1/R2)";

 "Schalk I s.89 Bsp 98a (1) (1/R=1/R1+1/R2)";

 "Schalk I s.89 Bsp 98a (1) (1/R=1/R1+1/R2)";

 (*ER-9*)

 val fmz = ["equality (1/R=1/R1+1/R2)",

 	   "solveFor R1","solutions L"];

 val (dI',pI',mI') = ("RatEq",["univariate","equation"],["no_met"]);

 (*val p = e_pos'; val c = []; 

 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));

 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)

 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 if f = Form'

       (FormKF

         (~1, EdUndef, 0, Nundef, "-1 * R * R2 + (R2 + -1 * R) * R1 = 0"))then()

 else error "rlang.sml: diff.behav. in Schalk I s.89 Bsp 98a (1)";

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[R1 = R * R2 / (R2 + -1 * R)]")) => ()

 	 | _ => error "rlang.sml: diff.behav. in 98a(1) [R1 = ...]";

 if get_assumptions_ pt p = [str2term"R * R2 * R2 ~= (R2 + -1 * R) * 0",

 			    str2term"R2 + -1 * R ~= 0",

 			    str2term"R2 + -1 * R ~= 0"] 

     then writeln "asm should be simplified"

 else error "rlang.sml: diff.behav. in 98a(1) asm";

 (*-----------------  Schalk I s.89 Bsp 104a(1) ------------------------*)

 "Schalk I s.89 Bsp 104a (1) (y^^^2=2*p*x)";

 "Schalk I s.89 Bsp 104a (1) (y^^^2=2*p*x)";

 "Schalk I s.89 Bsp 104a (1) (y^^^2=2*p*x)";

 (*ER-13 + EO-11 ?!?*)

 val fmz = ["equality (y^^^2=2*p*x)",

 	   "solveFor p","solutions L"];

 val (dI',pI',mI') = ("PolyEq",["univariate","equation"],["no_met"]);

 (*val p = e_pos'; val c = []; 

 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));

 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)

 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt; 

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 case f of Form' (FormKF (_,_,0,_,"[p = y ^^^ 2 / (2 * x)]")) => ()

 	 | _ => error "rlang.sml: diff.behav. in  Schalk I s.89 Bsp 104a (1) [p = y^2/(2*x)]";

 if get_assumptions_ pt p = [str2term"-2 * x ~= 0"] 

 then writeln"should be x ~= 0\nshould be x ~= 0\nshould be x ~= 0\n" 

 else error "rlang.sml: diff.behav. in  I s.89 Bsp 104a(1) asm";

 (*-----------------  Schalk I s.89 Bsp 104a(2) ------------------------*)

 "Schalk I s.89 Bsp 104a (2) (y^^^2=2*p*x)";

 "Schalk I s.89 Bsp 104a (2) (y^^^2=2*p*x)";

 "Schalk I s.89 Bsp 104a (2) (y^^^2=2*p*x)";

 (*EO ??*)

 val fmz = ["equality (y^^^2=2*p*x)",

 	   "solveFor y","solutions L"];

 val (dI',pI',mI') = ("PolyEq",["univariate","equation"],["no_met"]);

 (*val p = e_pos'; 

 val c = []; 

 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));

 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)

 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 case f of Form' (FormKF (_,_,0,_,"[y = sqrt (2 * p * x), y = -1 * sqrt (2 * p * x)]")) => ()

 | _ => error "rlang.sml: diff.behav. Schalk I s.89 Bsp 104a(2) [x = ]";

 if get_assumptions_ pt p = [str2term"0 <= -1 * (-2 * p * x)",

                             str2term"0 <= -1 * (-2 * p * x)"] 

 then writeln "asm should be simplified\nshould be simplified"

 else error "rlang.sml: diff.behav. in I s.89 Bsp 104a(2) asm";

 (*-----------------  Schalk I s.90 Bsp 118a (1) ------------------------*)

 "Schalk I s.90 Bsp 118a (1) (b^^^2*x^^^2 + a^^^2*y^^^2 = a^^^2*b^^^2)";

 "Schalk I s.90 Bsp 118a (1) (b^^^2*x^^^2 + a^^^2*y^^^2 = a^^^2*b^^^2)";

 "Schalk I s.90 Bsp 118a (1) (b^^^2*x^^^2 + a^^^2*y^^^2 = a^^^2*b^^^2)";

 (*EO-8*)

 val fmz = ["equality (b^^^2*x^^^2 + a^^^2*y^^^2 = a^^^2*b^^^2)",

 	   "solveFor x","solutions L"];

 val (dI',pI',mI') = ("PolyEq",["univariate","equation"],["no_met"]);

 (*val p = e_pos'; 

 val c = []; 

 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));

 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)

 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;f2str f;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;f2str f;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;f2str f;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;f2str f;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;f2str f;get_assumptions_ pt p;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;f2str f;get_assumptions_ pt p;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;f2str f;get_assumptions_ pt p;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;f2str f;get_assumptions_ pt p;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;f2str f;terms2str (*WN1104changed*) (get_assumptions_ pt p);

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;f2str f;terms2str (*WN1104changed*) (get_assumptions_ pt p);

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;f2str f;get_assumptions_ pt p;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;f2str f;get_assumptions_ pt p;

 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = sqrt ((a ^^^ 2 * b ^^^ 2 + -1 * a ^^^ 2 * y ^^^ 2) / b ^^^ 2),\n x = -1 * sqrt ((a ^^^ 2 * b ^^^ 2 + -1 * a ^^^ 2 * y ^^^ 2) / b ^^^ 2)]")) => writeln"should be simplified MG"

 | _ => error "rlang.sml: diff.behav. in  Schalk I s.89 Bsp 118a(2) [x = ]";

 val asms = get_assumptions_ pt p;

 if asms = 

   [str2term"0 * b ^^^ 2 <= -1 * (a ^^^ 2 * y ^^^ 2 + -1 * a ^^^ 2 * b ^^^ 2)",

    str2term"b ^^^ 2 ~= 0",

    str2term"0 * b ^^^ 2 <= -1 * (a ^^^ 2 * y ^^^ 2 + -1 * a ^^^ 2 * b ^^^ 2)",

    str2term"b ^^^ 2 ~= 0"] then writeln"should be simplified MG"

 else error "rlang.sml: diff.behav. in Schalk I s.89 Bsp 118a(2) asms";

 (*-----------------  Schalk I s.102 Bsp 268(1) ------------------------*)

 "Schalk I s.102 Bsp 268(1) (A = (1/2)*(x1*(y2-y3)+x2*(y3 - y1)+x3*(y1 - y2)))";

 "Schalk I s.102 Bsp 268(1) (A = (1/2)*(x1*(y2-y3)+x2*(y3 - y1)+x3*(y1 - y2)))";

 "Schalk I s.102 Bsp 268(1) (A = (1/2)*(x1*(y2-y3)+x2*(y3 - y1)+x3*(y1 - y2)))";

 (*ER-14*)

 val fmz = ["equality (A = (1/2)*(x1*(y2 - y3)+x2*(y3 - y1)+x3*(y1 - y2)))",

 	   "solveFor x2","solutions L"];

 val (dI',pI',mI') = ("PolyEq",["univariate","equation"],["no_met"]);

 (*val p = e_pos'; 

 val c = []; 

 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));

 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)

 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x2 =\n (-2 * A + x1 * y2 + x3 * y1 + -1 * x1 * y3 + -1 * x3 * y2) /\n (y1 + -1 * y3)]")) => ()

 | _ => error "rlang.sml: diff.behav. Schalk I s.102 Bsp 268(1) [x2=...]";

 if get_assumptions_ pt p = [str2term"y1 / 2 + -1 * y3 / 2 ~= 0"] then ()

 else error "rlang.sml: diff.behav. in I s.102 Bsp 268(1) asm";

 (*--------------------  Schalk II ----------------------------*)

 (*--------------------  Schalk II ----------------------------*)

 (*--------------------  Schalk II ----------------------------*)

 (*--------------------  Schalk II ----------------------------*)

 (*--------------------  Schalk II ----------------------------*)

 (*-----------------  Schalk II s.56 Bsp 67b ------------------------*)

 "Schalk II s.56 Bsp 67b (4*sqrt(4*x+1)=3*sqrt(7*x+2))";

 "Schalk II s.56 Bsp 67b (4*sqrt(4*x+1)=3*sqrt(7*x+2))";

 "Schalk II s.56 Bsp 67b (4*sqrt(4*x+1)=3*sqrt(7*x+2))";

 (*EO*)

 val fmz = ["equality (4*sqrt(4*x+1)=3*sqrt(7*x+2))",

 	   "solveFor x","solutions L"];

 val (dI',pI',mI') = ("RootEq",["univariate","equation"],["no_met"]);

 (*val p = e_pos'; 

 val c = []; 

 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));

 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)

 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; f2str f;

 if f = Form' (FormKF (~1, EdUndef, 0, Nundef, "-2 + x = 0")) then ()

 else error "rlang.sml: diff.behav. in Schalk II s.56 Bsp 67b";

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 2]")) => ()

 	 | _ => error "rlang.sml: diff.behav. in  Schalk II s.56 Bsp 67b [x=2]";

 (*-----------------  Schalk II s.56 Bsp 68a ------------------------*)

 "Schalk II s.56 Bsp 68a (5*sqrt(x) - 1 = 7*sqrt(x) - 5)";

 "Schalk II s.56 Bsp 68a (5*sqrt(x) - 1 = 7*sqrt(x) - 5)";

 "Schalk II s.56 Bsp 68a (5*sqrt(x) - 1 = 7*sqrt(x) - 5)";

 val fmz = ["equality (5*sqrt(x) - 1 = 7*sqrt(x) - 5)",

 	   "solveFor x","solutions L"];

 val (dI',pI',mI') = ("RootEq",["univariate","equation"],["no_met"]);

 (*val p = e_pos'; 

 val c = []; 

 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));

 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)

 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];

 (* val nxt = ("Model_Problem",Model_Problem ["normalize","root'","univariate","equation"])*)

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 (* val nxt = ("Model_Problem",Model_Problem ["sq","root'","univariate","equation"]) *)

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 (* val nxt = ("Model_Problem",Model_Problem ["sq","root'","univariate","equation"]) *)

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 get_assumptions_ pt p;

 (* val nxt = ("Model_Problem",  Model_Problem ["normalize","polynomial","univariate","equation"])*)

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 if f = Form'

       (FormKF

          (~1, EdUndef, 0, Nundef, "256 + -2368 * x + 576 * x ^^^ 2 = 0"))then()

 else error "rlang.sml: diff.behav. in Schalk II s.56 Bsp 68a";

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 get_assumptions_ pt p;

 (* val nxt = ("Model_Problem",  Model_Problem

      ["abcFormula","degree_2","polynomial","univariate","equation"])*)

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 get_assumptions_ pt p;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 if f = Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 4, x = 1 / 9]")) 

 then writeln "only [x = 4] !\nonly [x = 4] !\nonly [x = 4] !\n"

 else error "rlang.sml: diff.behav. in II 68a";

 val asms = get_assumptions_ pt p;

 if terms2str (*WN1104changed*) asms = 

 "[0 <= (25 * (1 / 9) + -1 * (16 + 49 * (1 / 9))) * -56,\

  \0 <= 1 / 9,\

  \0 <= 1 / 9,\

  \0 <= (-5 + 7 * sqrt (1 / 9) + 1) * 5,\

  \0 <= 1 / 9,\

  \0 <= (25 * (1 / 9) + -1 * (16 + 49 * (1 / 9))) * -56,\

  \0 <= 1 / 9]"

 (*WN050916 before correction 'rewrite__set_ called with 'Erls' for ..'

   thus: maybe the rls for the asms is Erls ??:

    [(str2term"0 <= (25 * (1 / 9) + -1 * (16 + 49 * (1 / 9))) * -56", []),

     (str2term"9 ~= 0", []),

     (str2term"0 <= (-5 + 7 * sqrt (1 / 9) + 1) * 5", []),

     (str2term"9 ~= 0", []),

     (str2term"0 <= (25 * (1 / 9) + -1 * (16 + 49 * (1 / 9))) * -56", [])]*)

     then "should get True * False!!!"

 else error "rlang.sml: diff.behav. in II 68a asms";

 (*-----------------  Schalk II s.56 Bsp 73b ------------------------*)

 "Schalk II s.56 Bsp 73b (sqrt(x+1)+sqrt(4*x+4)=sqrt(9*x+9))";

 "Schalk II s.56 Bsp 73b (sqrt(x+1)+sqrt(4*x+4)=sqrt(9*x+9))";

 "Schalk II s.56 Bsp 73b (sqrt(x+1)+sqrt(4*x+4)=sqrt(9*x+9))";

 (*EO-2*)

 val fmz = ["equality (sqrt(x+1)+sqrt(4*x+4)=sqrt(9*x+9))",

 	   "solveFor x","solutions L"];

 val (dI',pI',mI') = ("RootEq",["univariate","equation"],["no_met"]);

 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 (*"13 + 13 * x + -2 * sqrt ((4 + 4 * x) * (9 + 9 * x)) = 1 + x" 

 -> Subproblem ("RootEq", ["univariate", ...])*)

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 (*"144 + 288 * x + 144 * x ^^^ 2 = 144 + x ^^^ 2 + 288 * x + 143 * x ^^^ 2"

 -> Subproblem ("RootEq", ["univariate", ...])*)

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 if f = Form' (FormKF (~1, EdUndef, 0, Nundef, "0 = 0")) then ()

 else error "rlang.sml: diff.behav. in Schalk II s.56 Bsp 73b";

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val asm = get_assumptions_ pt p;

 if asm=[] andalso f = Form' (FormKF (~1,EdUndef,0,Nundef,"UniversalList")) andalso nxt = ("End_Proof'",End_Proof') then ()

 else error "rlang.sml: diff.behav. in UniversalList 2";

 (*-----------------  Schalk II s.56 Bsp 74a ------------------------*)

 "Schalk II s.56 Bsp 74a (sqrt(4*x+1) - sqrt(x+3) = sqrt(x - 2))";

 "Schalk II s.56 Bsp 74a (sqrt(4*x+1) - sqrt(x+3) = sqrt(x - 2))";

 "Schalk II s.56 Bsp 74a (sqrt(4*x+1) - sqrt(x+3) = sqrt(x - 2))";

 (*EO-3*)

 val fmz = ["equality (sqrt(4*x+1) - sqrt(x+3) = sqrt(x - 2))",

 	   "solveFor x","solutions L"];

 val (dI',pI',mI') = ("RootEq",["univariate","equation"],["no_met"]);

 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 (*4 + 5 * x + -2 * sqrt (3 + 13 * x + 4 * x ^^^ 2) = -2 + x" 

 -> Subproblem ("RootEq", ["univariate", ...])*)

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 (*"12 + 52 * x + 16 * x ^^^ 2 = 36 + x ^^^ 2 + 48 * x + 15 * x ^^^ 2"

 -> Subproblem ("RootEq", ["univariate", ...])*)

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 if f = Form' (FormKF (~1, EdUndef, 0, Nundef, "-24 + 4 * x = 0")) then ()

 else error "rlang.sml: diff.behav. in Schalk II s.56 Bsp 74a";

 (*-> ubproblem ("PolyEq", ["degree_1", ...]*)

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 6]")) => ()

 	 | _ => error "rlang.sml: diff.behav. in  Schalk II s.56 Bsp 74a [x = 6]";

 (*-----------------  Schalk II s.56 Bsp 77b ------------------------*)

 "Schalk II s.56 Bsp 77b (sqrt(x+12)+sqrt(x - 3) = sqrt(x + 32) - sqrt(5+x))";

 "Schalk II s.56 Bsp 77b (sqrt(x+12)+sqrt(x - 3) = sqrt(x + 32) - sqrt(5+x))";

 "Schalk II s.56 Bsp 77b (sqrt(x+12)+sqrt(x - 3) = sqrt(x + 32) - sqrt(5+x))";

 (*EO-4*)

 val fmz = ["equality (sqrt(x+12)+sqrt(x - 3) = sqrt(x + 32) - sqrt(5+x))",

 	   "solveFor x","solutions L"];

 val (dI',pI',mI') = ("RootEq",["univariate","equation"],["no_met"]);

 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];

 (* val nxt = ("Model_Problem",Model_Problem ["sq","root'","univariate","equation"]) *)

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 (* val nxt = ("Model_Problem",Model_Problem ["sq","root'","univariate","equation"]) *)

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; f2str f;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; 

 (* val nxt = ("Model_Problem",Model_Problem ["sq","root'","univariate","equation"]) *)

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 (*val nxt = ("Model_Problem", 

  Model_Problem ["normalize","polynomial","univariate","equation"])*)

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 (*val (p,_,f,nxt,_,pt) = me nxt p [1] pt; since MGs norm_Rational*)

 if f = Form'(FormKF (~1, EdUndef, 0, Nundef, "451584 + -112896 * x = 0"))then()

 else error "rlang.sml: diff.behav. in Schalk II s.56 Bsp 77b";

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 (* val nxt = ("Model_Problem",

    Model_Problem ["degree_1","polynomial","univariate","equation"])*)

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[]")) => ()

 	 | _ => error "rlang.sml: diff.behav. in  Schalk II s.56 Bsp 77b []";

 (*added 040209 at introducing MGs norm_Rational ?!*)

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 (*-----------------  Schalk II s.66 Bsp 4 ------------------------*)

 "Schalk II s.66 Bsp 4 ((6*x - 9)*(5*x+7) - (4*x+7)*(3*x - 6) = 429)";

 "Schalk II s.66 Bsp 4 ((6*x - 9)*(5*x+7) - (4*x+7)*(3*x - 6) = 429)";

 "Schalk II s.66 Bsp 4 ((6*x - 9)*(5*x+7) - (4*x+7)*(3*x - 6) = 429)";

 (*EP*)

 val fmz = ["equality ((6*x - 9)*(5*x+7) - (4*x+7)*(3*x - 6) = 429)",

 	   "solveFor x","solutions L"];

 val (dI',pI',mI') = ("PolyEq",["univariate","equation"],["no_met"]);

 (*val p = e_pos'; 

 val c = []; 

 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));

 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)

 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 case f of   Form' (FormKF (_,_,0,_,"[x = 5, x = -5]")) => ()

   | _ => error "rlang.sml: diff.behav. in  Schalk II s.66 Bsp 4 []";

 (*-----------------  Schalk II s.66 Bsp 8a ------------------------*)

 "Schalk II s.66 Bsp 8a ((x - 4)/(x+4) = (1 - x)/(1+x))";

 (*ER-15*)

 val fmz = ["equality ((x - 4)/(x+4) = (1 - x)/(1+x))",

 	   "solveFor x","solutions L"];

 val (dI',pI',mI') = ("RatEq",["univariate","equation"],["no_met"]);

 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; f2str f;

 (*"(-4 + x) * (1 + x) = (1 + -1 * x) * (4 + x)"

 -> Subproblem ("RatEq", ["univariate", ...])*)

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 if f = Form' (FormKF (~1, EdUndef, 0, Nundef, "-8 + 2 * x ^^^ 2 = 0")) then ()

 else error "rlang.sml: diff.behav. in Schalk II s.66 Bsp 8a";

 (*-> Subproblem ("PolyEq", ["polynomial", ...])*)

 (* 

  val Form' (FormKF (~1, EdUndef, 0, Nundef, str)) = f;

  *)

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 2, x = -2]")) => ()

 	 | _ => error "rlang.sml: diff.behav. in  Schalk II s.66 Bsp 8a [x = 2, x = -2]";

 (*-----------------  Schalk II s.66 Bsp 10b ------------------------*)

 "Schalk II s.66 Bsp 10b (1/(x^^^2 - 9)+(2*x+3)/(x+3)=(3*x+4)/(x - 3))";

 "Schalk II s.66 Bsp 10b (1/(x^^^2 - 9)+(2*x+3)/(x+3)=(3*x+4)/(x - 3))";

 "Schalk II s.66 Bsp 10b (1/(x^^^2 - 9)+(2*x+3)/(x+3)=(3*x+4)/(x - 3))";

 val fmz = ["equality (1/(x^^^2 - 9)+(2*x+3)/(x+3)=(3*x+4)/(x - 3))",

 	   "solveFor x","solutions L"];

 val (dI',pI',mI') = ("RatEq",["univariate","equation"],["no_met"]);

 (*val p = e_pos'; 

 val c = []; 

 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));

 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)

 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 if f = Form'

       (FormKF

          (~1,

             EdUndef,

             0,

             Nundef,

             "60 + 28 * x + -13 * x ^^^ 2 + -1 * x ^^^ 3 = 0")) then ()

 else error "rlang.sml: diff.behav. in Schalk II s.66 Bsp 10b";

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 (*60 + 28 * x + -13 * x ^^^ 2 + -1 * x ^^^ 3 = 0 ... degree 3 not solvable*)

 (*-----------------  Schalk II s.66 Bsp 20a ------------------------*)

 (*EO-6*)

 "Schalk II s.66 Bsp 20a (sqrt(29 - sqrt (x^^^2 - 9))=5)";

 "Schalk II s.66 Bsp 20a (sqrt(29 - sqrt (x^^^2 - 9))=5)";

 "Schalk II s.66 Bsp 20a (sqrt(29 - sqrt (x^^^2 - 9))=5)";

 val fmz = ["equality (sqrt(29 - sqrt(x^^^2 - 9))=5)",

 	   "solveFor x","solutions L"];

 val (dI',pI',mI') = ("RootEq",["univariate","equation"],["no_met"]);

 (*val p = e_pos'; 

 val c = []; 

 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));

 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)

 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 if f = Form' (FormKF (~1, EdUndef, 0, Nundef, "-25 + x ^^^ 2 = 0")) then ()

 else error "rlang.sml: diff.behav. in Schalk II s.66 Bsp 20a";

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 5, x = -5]")) => ()

 	 | _ => error "rlang.sml: diff.behav. in  Schalk II s.66 Bsp 20a [x = 5, x = -5]";

 (*-----------------  Schalk II s.66 Bsp 23b ------------------------*)

 "Schalk II s.66 Bsp 23b (2*sqrt(261 - x) - sqrt(2+2*x)=sqrt(2)*sqrt(5 - 3*x))";

 "Schalk II s.66 Bsp 23b (2*sqrt(261 - x) - sqrt(2+2*x)=sqrt(2)*sqrt(5 - 3*x))";

 "Schalk II s.66 Bsp 23b (2*sqrt(261 - x) - sqrt(2+2*x)=sqrt(2)*sqrt(5 - 3*x))";

 (*EO WN060310 something wrong:

 ([6, 6, 3, 1], Frm) "-1064944 + 32 * x + -48 * x ^^^ 2 = 0"

 	### or2list False

 ([6, 6, 3, 1], Res) "HOL.False"

 *)

 val fmz = ["equality (2*sqrt(261 - x) - sqrt(2+2*x)=sqrt(2)*sqrt(5 - 3*x))",

 	   "solveFor x","solutions L"];

 val (dI',pI',mI') = ("RootEq",["univariate","equation"],["no_met"]);

 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; f2str f;

 if f = Form'

       (FormKF

        (~1, EdUndef, 0, Nundef, "-1064944 + 32 * x + -48 * x ^^^ 2 = 0"))then()

 else error "rlang.sml: diff.behav. in Schalk II s.66 Bsp 23b";

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 case f of Form' (FormKF (~1,EdUndef,_,Nundef,"[]")) => ()

 	 | _ => error "rlang.sml: diff.behav. in  Schalk II s.66 Bsp 23b []";

 (*-----------------  Schalk II s.66 Bsp 28a ------------------------*)

 "Schalk II s.66 Bsp 28a (A=(c/d)*sqrt(4*a^^^2 - c^^^2))";

 "Schalk II s.66 Bsp 28a (A=(c/d)*sqrt(4*a^^^2 - c^^^2))";

 "Schalk II s.66 Bsp 28a (A=(c/d)*sqrt(4*a^^^2 - c^^^2))";

 val fmz = ["equality (A=(c/d)*sqrt(4*a^^^2 - c^^^2))",

 	   "solveFor a","solutions L"];

 val (dI',pI',mI') = ("RootEq",["univariate","equation"],["no_met"]);

 (*val p = e_pos'; 

 val c = []; 

 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));

 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)

 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 (*if f = Form'

       (FormKF

          (~1,

             EdUndef,

             0,

             Nundef,

             "c ^^^ 4 / d ^^^ 2 + A ^^^ 2 * d ^^^ 2 / d ^^^ 2 +\n-4 * c ^^^ 2 / d ^^^ 2 * a ^^^ 2 =\n0")) then ()*)

 if f2str f = 

    "c ^^^ 4 / d ^^^ 2 + A ^^^ 2 / 1 + -4 * c ^^^ 2 / d ^^^ 2 * a ^^^ 2 = 0"

 then () else error "rlang.sml: diff.behav. in Schalk II s.66 Bsp 28a";

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[a = sqrt ((c ^^^ 4 + A ^^^ 2 * d ^^^ 2) / (4 * c ^^^ 2)),\n a = -1 * sqrt ((c ^^^ 4 + A ^^^ 2 * d ^^^ 2) / (4 * c ^^^ 2))]")) => ()

 | _ => error "rlang.sml: diff.behav. in  Schalk II s.66 Bsp 28a [a=...]";

 (*-----------------  Schalk II s.68 Bsp 52b ------------------------*)

 "Schalk II s.68 Bsp 52b (1/(x - a+b)=1/x - 1/a + 1/b)";

 val fmz = ["equality (1/(x - a+b)=1/x - 1/a + 1/b)",

 	   "solveFor x","solutions L"];

 val (dI',pI',mI') = ("RatEq",["univariate","equation"],["no_met"]);

 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];

 (* val nxt = ("Model_Problem",Model_Problem ["rational","univariate","equation"])*)

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 (*val nxt = ("Specify_Theory",Specify_Theory "RatEq")*)

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 (*val p = ([3],Res)

 val f="1 * (a * (b * x)) = (a * b + (a * x + -1 * (b * x))) * (b + (x + -1 * a)

 val nxt = Subproblem ("RatEq",["univariate","equation"]))*)

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 (*val nxt = ("Specify_Theory",Specify_Theory "PolyEq")*)

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 (* nxt = Specify_Problem ["normalize","polynomial","univariate","equation"])*)

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 (*val (p,_,f,nxt,_,pt) = me nxt p [1] pt; at introducing of MGs norm_Rational*)

 (*val p = ([4,5],Res)  val f ="b * a ^^^ 2 + -1 * a * b ^^^ 2 + (a ^^^ 2 + b ^^^ 2 + -2 * a * b) * x +\n(b + -1 * a) * x ^^^ 2 =\n0"))

 val nxt = Subproblem ("PolyEq",["polynomial","univariate","equation"]))*)

 if f = Form'

       (FormKF

          (~1,

             EdUndef,

             0,

             Nundef,

             "b * a ^^^ 2 + -1 * a * b ^^^ 2 + (a ^^^ 2 + b ^^^ 2 + -2 * a * b) * x +\n(b + -1 * a) * x ^^^ 2 =\n0")) then ()

 else error "rlang.sml: diff.behav. in chalk I s.87 Bsp 38b";

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 (*val nxt = ("Specify_Theory",Specify_Theory "PolyEq")*)

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 (*Specify_Problem["abcFormula","degree_2","polynomial","univariate","equation*)

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 (*val (p,_,f,nxt,_,pt) = me nxt p [1] pt;introducing MGs norm_Rational*)

 (*val p = ([4,6,5],Res) val f ="[x =\n (2 * a * b + -1 * a ^^^ 2 + -1 * b ^^^ 2 +\n  sqrt\n   (a ^^^ 4 + b ^^^ 4 + -4 * a * a * b ^^^ 2 + -4 * a * b * a ^^^ 2 +\n    -4 * b * b * a ^^^ 2 +\n    4 * a * a * b ^^^ 2 +\n    4 * a * b * a ^^^ 2 +\n    2 * a ^^^ 2 * b ^^^ 2)) /\n (-2 * a + 2 * #"

 nx Check_Postcond["abcFormula","degree_2","polynomial","univariate","equation*)

 (*9.9.03:   -"-  ["normalize","polynomial","univar...*)

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 (*val p = ([4,6],Res)

 val nxt =Check_Postcond ["normalize","polynomial","univariate","equation"])*)

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;(*1 additional for MGs norm_Rational*)

 if p = ([],Res) andalso f = Form' (FormKF (~1,EdUndef,0,Nundef,

 "[x =\n (2 * a * b + -1 * a ^^^ 2 + -1 * b ^^^ 2 +\n  sqrt\n   (a ^^^ 4 + b ^^^ 4 + -4 * a * a * b ^^^ 2 + -4 * a * b * a ^^^ 2 +\n    -4 * b * b * a ^^^ 2 +\n    4 * a * a * b ^^^ 2 +\n    4 * a * b * a ^^^ 2 +\n    2 * a ^^^ 2 * b ^^^ 2)) /\n (-2 * a + 2 * b),\n x =\n (2 * a * b + -1 * a ^^^ 2 + -1 * b ^^^ 2 +\n  -1 *\n  sqrt\n   (a ^^^ 4 + b ^^^ 4 + -4 * a * a * b ^^^ 2 + -4 * a * b * a ^^^ 2 +\n    -4 * b * b * a ^^^ 2 +\n    4 * a * a * b ^^^ 2 +\n    4 * a * b * a ^^^ 2 +\n    2 * a ^^^ 2 * b ^^^ 2)) /\n (-2 * a + 2 * b)]")) andalso nxt = ("End_Proof'",End_Proof') then writeln"simplify MG"

 else error "rlang.sml: diff.behav. in rational-a-b";

 (*-----------------  Schalk II s.68 Bsp 56a ------------------------*)

 "Schalk II s.68 Bsp 56a ((a+b*x)/(a-b*x) - (a - b*x)/(a+b*x)= (4*a*b)/(a^^^2 - b^^^2))";

 val fmz = ["equality ((a+b*x)/(a-b*x) - (a - b*x)/(a+b*x)= (4*a*b)/(a^^^2 - b^^^2))","solveFor x","solutions L"];

 val (dI',pI',mI') = ("RatEq",["univariate","equation"],["no_met"]);

 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];

 (* val nxt = ("Model_Problem",Model_Problem ["rational","univariate","equation"]) *)

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 (*SK loops with poly:

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 ... with sml-nj:

  (a + b * x) / (a + -1 * (b * x)) + (-1 * a + b * x) / (a + b * x) =

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

 add_fractions_p wird nicht angewendet, weil ...

 add_fract terminiert nicht: 030603

 siehe Rational.ML rational.sml

 *)

 (*

 "(a + b * x) / (a + -1 * (b * x)) + -1 * (a + -1 * (b * x)) / (a + b * x) =\n4 * a * b / (a ^^^ 2 + -1 * b ^^^ 2)"

 val nxt = ("Rewrite_Set",Rewrite_Set "make_ratpoly") : string * tac           

 "(a + b * x) / (a + -1 * b * x) + (-1 * a + b * x) / (a + b * x) =\n4 *

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

 val t = str2term"(a + b * x) / (a + -1 * (b * x)) + -1 * (a + -1 * (b * x)) / (a + b * x) =\n4 * a * b / (a ^^^ 2 + -1 * b ^^^ 2)";

 trace_rewrite := false;

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

 term2str t';

 trace_rewrite:=false;

 #  rls: norm_Rational on: (a + b * x) / (a + -1 * (b * x)) + -1 * (a + -1 * (b * x)) / (a + b * x) = 4 * a * b / (a ^^^ 2 + -1 * b ^^^ 2)

 ##  rls: discard_minus on: 

 ##  rls: powers on:

 ##  rls: rat_mult_divide on:

 ##  rls: expand on:

 ##  rls: reduce_0_1_2 on:

 ##  rls: order_add_mult on:

 ###  try thm: mult_commute

 ===  rewrites to: (a + b * x) / (a + -1 * (b * x)) + (-1 * a + -1 * (-1 * (b * x))) / (a + b * x) = b * (4 * a) / (a ^^^ 2 + -1 * b ^^^ 2)

 ###  try thm: real_mult_left_commute

 ===  rewrites to: (a + b * x) / (a + -1 * (b * x)) + (-1 * a + -1 * (-1 * (b * x))) / (a + b * x) = 4 * (b * a) / (a ^^^ 2 + -1 * b ^^^ 2)

 ###  try thm: mult_commute

 ===  rewrites to: (a + b * x) / (a + -1 * (b * x)) + (-1 * a + -1 * (-1 * (b * x))) / (a + b * x) = 4 * (a * b) / (a ^^^ 2 + -1 * b ^^^ 2)

 ###  try calc: op *'

 ===  calc. to: (a + b * x) / (a + -1 * (b * x)) + (-1 * a + 1 * (b * x)) / (a +b * x) = 4 * (a * b) / (a ^^^ 2 + -1 * b ^^^ 2)

 ##  rls: add_fractions_p on: (a + b * x) / (a + -1 * (b * x)) + (-1 * a + 1 * (b * x)) / (a + b * x) = 

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

 !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!GC

 ##  rls: discard_minus on:

 ##  rls: powers on:

 ##  rls: rat_mult_divide on:

 ##  rls: expand on:

 ##  rls: reduce_0_1_2 on:

 ###  try thm: real_mult_1

 ===  rewrites to: (a + b * x) / (a + -1 * (b * x)) + (-1 * a + b * x) / (a + b * x) = 4 * (a * b) / (a ^^^ 2 + -1 * b ^^^ 2)

 ##  rls: order_add_mult on:

 ##  rls: add_fractions_p on: (a + b * x) / (a + -1 * (b * x)) + (-1 * a + b * x) / (a + b * x) =

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

 !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!GC

 ##  rls: discard_minus on:

 ##  rls: powers on:

 ##  rls: rat_mult_divide on:

 ##  rls: expand on:

 ##  rls: reduce_0_1_2 on:

 ##  rls: order_add_mult on:

 ##  rls: collect_numerals on:

 ##  rls: add_fractions_p on: (a + b * x) / (a + -1 * (b * x)) + (-1 * a + b * x) / (a + b * x) =

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

 !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!GC

 *)

 (*-----------------  Schalk II s.68 Bsp 61b ------------------------*)

 "Schalk II s.68 Bsp 61b (sqrt(x+a)+sqrt(b - x)=sqrt(a+b))";

 val fmz = ["equality (sqrt(x+a)+sqrt(b - x)=sqrt(a+b))",

 	   "solveFor x","solutions L"];

 val (dI',pI',mI') = ("RootEq",["univariate","equation"],["no_met"]);

 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];

 (* val nxt = ("Model_Problem",Model_Problem ["sq","root'","univariate","equation"])*)

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 (* val nxt = ("Model_Problem",Model_Problem ["sq","root'","univariate","equation"])*)

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 (*val nxt = ("Model_Problem",

    Model_Problem ["normalize","polynomial","univariate","equation"])*)

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 if f = Form'

       (FormKF

          (~1,

             EdUndef,

             0,

             Nundef,

             (*"-4 * b ^^^ 2 + -4 * a * b + 4 * b ^^^ 2 + 8 * a * b +\n(-2 * a + -4 * a + -4 * b + 2 * a + 8 * b) * x +\n-4 * x ^^^ 2 =\n0" before MG*)

 	    "4 * a * b + (-4 * a + 4 * b) * x + -4 * x ^^^ 2 = 0")) then ()

 else error "rlang.sml: diff.behav. in Schalk II s.68 Bsp 61b";

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 (*val nxt = ("Model_Problem", Model_Problem

      ["abcFormula","degree_2","polynomial","univariate","equation"])*)

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 (* f= ... "-4 * b ^^^ 2 + -4 * a * b + 4 * b ^^^ 2 + 8 * a * b + 

            (-2 * a + -4 * a + -4 * b + 2 * a + 8 * b) * x + -4 * x ^^^ 2 =0"*)

 (*val nxt = ("Rewrite_Set_Inst",Rewrite_Set_Inst ([#],"d2_polyeq_abcFormula_simplify"))*)

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 (*if f = Form' (FormKF (~1,EdUndef,0,Nundef, with norm_Rational before MG

 "[x =\n (-2 * a + -4 * b + 6 * a +\n  sqrt\n   (32 * a * b + -16 * a ^^^ 2 + -48 * b ^^^ 2 + 24 * a ^^^ 2 +\n    64 * b ^^^ 2 +\n    8 * a ^^^ 2)) /\n -8,\n x =\n (-2 * a + -4 * b + 6 * a +\n  -1 *\n  sqrt\n   (32 * a * b + -16 * a ^^^ 2 + -48 * b ^^^ 2 + 24 * a ^^^ 2 +\n    64 * b ^^^ 2 +\n    8 * a ^^^ 2)) /\n -8]")) then writeln"simplify MG"*)

 if f = Form' (FormKF (~1,EdUndef,0,Nundef,"[x =\n (-4 * b + 4 * a + sqrt (32 * a * b + 16 * a ^^^ 2 + 16 * b ^^^ 2)) / -8,\n x =\n (-4 * b + 4 * a + -1 * sqrt (32 * a * b + 16 * a ^^^ 2 + 16 * b ^^^ 2)) /\n -8]")) then ()

 else error "rlang.sml: diff.behav. Bsp 61b";

 (*WN.18.12.03: extreme run-time !!!*)

 (*-----------------  Schalk II s.68 Bsp 62b ------------------------*)

 "Schalk II s.68 Bsp 62b (sqrt((x+a)^^^2+(x - 2*b)^^^2)=a+2*b)";

 val fmz = ["equality (sqrt((x+a)^^^2+(x - 2*b)^^^2)=a+2*b)",

 	   "solveFor x","solutions L"];

 val (dI',pI',mI') = ("RootEq",["univariate","equation"],["no_met"]);

 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];

 (*val nxt = ("Model_Problem",Model_Problem ["sq","root'","univariate","equation"]) *)

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 (* val nxt = ("Model_Problem",

    Model_Problem ["normalize","polynomial","univariate","equation"])*)

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 if f = Form'

       (FormKF

          (~1,

             EdUndef,

             0,

             Nundef,

             "-4 * a * b + (-4 * b + 2 * a) * x + 2 * x ^^^ 2 = 0")) then ()

 else error "rlang.sml: diff.behav. in Schalk II s.68 Bsp 62b";

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 (*val nxt =  ("Model_Problem", Model_Problem

      ["abcFormula","degree_2","polynomial","univariate","equation"])*)

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 (*val f = ... "-4 * a * b + (-4 * b + 2 * a) * x + 2 * x ^^^ 2 = 0" *)

 (*val nxt =  ("Rewrite_Set_Inst",Rewrite_Set_Inst ([#],"d2_polyeq_abcFormula_simplify"))*)

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 (*val (p,_,f,nxt,_,pt) = me nxt p [1] pt;introduc.MGs norm_Rational*)

 if f = Form' (FormKF (~1,EdUndef,0,Nundef,

         "[x = (-2 * a + 4 * b + sqrt (16 * a * b + 16 * b ^^^ 2 + 4 * a ^^^ 2)) / 4,\n x =\n (-2 * a + 4 * b + -1 * sqrt (16 * a * b + 16 * b ^^^ 2 + 4 * a ^^^ 2)) / 4]")) then writeln "simplify MG"

 else error "rlang.sml: diff.behav. in II 62b [x=...]";

 val asms = get_assumptions_ pt p;

 if asms = [str2term"0 <= ((-2 * a + 4 * b + sqrt (16 * a * b + 16 * b ^^^ 2 + 4 * a ^^^ 2)) / 4 + a) ^^^ 2 + ((-2 * a + 4 * b + sqrt (16 * a * b + 16 * b ^^^ 2 + 4 * a ^^^ 2)) / 4 - 2 * b) ^^^ 2",

 	   str2term"0 <= a + 2 * b",

 	   str2term"8 * (-4 * a * b) <= (-4 * b + 2 * a) ^^^ 2",

 	   str2term"8 * (-4 * a * b) <= (-4 * b + 2 * a) ^^^ 2",

 	   str2term"0 <= ((-2 * a + 4 * b + -1 * sqrt (16 * a * b + 16 * b ^^^ 2 + 4 * a ^^^ 2)) / 4 + a) ^^^ 2 + ((-2 * a + 4 * b + -1 * sqrt (16 * a * b + 16 * b ^^^ 2 + 4 * a ^^^ 2)) / 4 - 2 * b) ^^^ 2",

 	   str2term"0 <= a + 2 * b",

 	   str2term"8 * (-4 * a * b) <= (-4 * b + 2 * a) ^^^ 2",

 	   str2term"8 * (-4 * a * b) <= (-4 * b + 2 * a) ^^^ 2"] 

 then writeln "should be simplified MG"

 else error "rlang.sml: diff.behav. in II 62b asms";

 "------ WN.TEST---------------------------------";

 "------ WN.TEST---------------------------------";

 "------ WN.TEST---------------------------------";

 (*EO-7*)

 val fmz = ["equality ((2*x+1)*x^^^2 = 0)",

 	   "solveFor x","solutions L"];

 val (dI',pI',mI') = ("PolyEq",["univariate","equation"],["no_met"]);

 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 (*

 val f = Form' (FormKF (~1,EdUndef,1,Nundef,"(2 * x + 1) * x ^^^ 2 = 0"))

 normiert nicht ... korr.WN:

 val t = str2term "(2*x+1)*x^^^2 = 0";

 val subst = [(str2term "bdv", str2term "x")];

 val SOME (t',_) = rewrite_set_inst_ thy false subst make_ratpoly_in t;

 if term2str t' = "x ^^^ 2 + 2 * x ^^^ 3 = 0" then () 

 else error "rlang.sml: 7";

 *)

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

 if f = Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 0, x = 0, x = -1 / 2]")) then()

 else error "rlang.sml WN.TEST new behaviour";

 "------ rlang.sml end---------------------------------";

 (*------------------------------vvv-Rewrite_Set "rat_eliminate"---------

 > trace_rewrite:=true;

 > val t = str2term 

   "(3 + -1 * x + 1 * x ^^^ 2) / (9 * x + -6 * x ^^^ 2 + 1 * x ^^^ 3) = 1 / x";

 > val SOME (t',asm) = 

       rewrite_ thy dummy_ord rateq_erls true rat_mult_denominator_both t;

 > term2str t'; terms2str asm;

 "(3 + -1 * x + 1 * x ^^^ 2) * x = 1 * (9 * x + -6 * x ^^^ 2 + 1 * x ^^^ 3)"

 "[\"9 * x + -6 * x ^^^ 2 + 1 * x ^^^ 3 ~= 0\",\"x ~= 0\"]"

 > trace_rewrite:=false;

   ------------------------------^^^-Rewrite_Set "rat_eliminate"---------*)

 "-------------------- WN.15.5.03: Pythagoras -------------------------------";

 "-------------------- WN.15.5.03: Pythagoras -------------------------------";

 "-------------------- WN.15.5.03: Pythagoras -------------------------------";

 (*EO-9*)

 val fmz = ["equality ((a/2)^^^2 + (b/2)^^^2 = r^^^2)",

 	   "solveFor a","solutions L"];

 val (dI',pI',mI') = ("PolyEq",["univariate","equation"],["no_met"]);

 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];

 (*   Model_Problem ["normalize","polynomial","univariate","equation"])*)

 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;

 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;

 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;

 val (p,_,f,nxt,_,pt) = me nxt p c pt;

 (*val nxt = ("Apply_Method",Apply_Method ["PolyEq","normalize_poly"])*)

 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;

 val (p,_,f,nxt,_,pt) = me nxt p c pt;

 (*val nxt = Subproblem ("PolyEq",["polynomial","univariate","equation"])*)

 val (p,_,f,nxt,_,pt) = me nxt p c pt;

 val (p,_,f,nxt,_,pt) = me nxt p c pt;

 (*val nxt =Model_Problem ["sq_only","degree_2","polynomial","univariate","equation"])*)

 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;

 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;

 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;

 val (p,_,f,nxt,_,pt) = me nxt p c pt;

 (*val nxt = Apply_Method ["PolyEq","solve_d2_polyeq_sqonly_equation"])*)

 val (p,_,f,nxt,_,pt) = me nxt p c pt;

 val (p,_,f,nxt,_,pt) = me nxt p c pt;

 val (p,_,f,nxt,_,pt) = me nxt p c pt;

 val (p,_,f,nxt,_,pt) = me nxt p c pt;

 val (p,_,f,nxt,_,pt) = me nxt p c pt;

 val (p,_,f,nxt,_,pt) = me nxt p c pt;

 val (p,_,f,nxt,_,pt) = me nxt p c pt;

 if f = Form' (FormKF (~1,EdUndef,0,Nundef,

 "[a = sqrt ((-1 * b ^^^ 2 + 4 * r ^^^ 2) / 1),\n a = -1 * sqrt ((-1 * b ^^^ 2 + 4 * r ^^^ 2) / 1)]")) andalso nxt = ("End_Proof'",End_Proof')

 then writeln"simplify result\nsimplify result\nsimplify result"

 else error "rlang.sml: diff.behav. in Pythagoras";

 val asms = get_assumptions_ pt p;

 (*if asms = [str2term"0 <= -4 * (b ^^^ 2 / 4 + -4 * r ^^^ 2 / 4)",

              str2term"0 <= -4 * (b ^^^ 2 / 4 + -4 * r ^^^ 2 / 4)"]*)

 if terms2str (*WN1104changed*) asms = 

    "[0 <= -4 * (b ^^^ 2 / 4 + -1 * r ^^^ 2 / 1),\

    \0 <= -4 * (b ^^^ 2 / 4 + -1 * r ^^^ 2 / 1)]"

 then writeln"simplify result\nsimplify result\nsimplify result"

 else error "rlang.sml: diff.behav. in Pythagoras asms";

 "-------------------- WN.15.5.03: equation within the maximum example ------";

 "-------------------- WN.15.5.03: equation within the maximum example ------";

 "-------------------- WN.15.5.03: equation within the maximum example ------";

 (*EO-10*)

 val fmz = ["equality (2*sqrt(r^^^2 - (u/2)^^^2) - u^^^2/(2*sqrt(r^^^2 - (u/2)^^^2))= 0)",

 	   "solveFor u","solutions L"];

 val (dI',pI',mI') = ("PolyEq",["univariate","equation"],["no_met"]);

 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];

 (*   Model_Problem ["normalize","root'","univariate","equation"])*)

 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;

 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;

 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;

 val (p,_,f,nxt,_,pt) = me nxt p c pt;

 (*val nxt = Apply_Method ["RootEq","norm_sq_root_equation"])     *)

 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;

 (*val nxt = Subproblem ("RootEq",["univariate","equation"]))*)

 val (p,_,f,nxt,_,pt) = me nxt p c pt;

 (*val nxt = Model_Problem ["sq","root'","univariate","equation"]) *)

 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;

 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;

 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;

 val (p,_,f,nxt,_,pt) = me nxt p c pt;

 (*val nxt = Apply_Method ["RootEq","solve_sq_root_equation"])     *)

 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;

 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;

 val (p,_,f,nxt,_,pt) = me nxt p c pt;

 (*val nxt = Subproblem ("RootEq",["univariate","equation"]))*)

 val (p,_,f,nxt,_,pt) = me nxt p c pt;

 (*val nxt = Model_Problem ["rational","univariate","equation"]) *)

 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;

 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;

 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;

 val (p,_,f,nxt,_,pt) = me nxt p c pt;

 (*val nxt = Apply_Method ["RootEq","solve_rat_equation"])     *)

 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;

 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;

 (*val nxt = Subproblem ("RootEq",["univariate","equation"]))*)

 val (p,_,f,nxt,_,pt) = me nxt p c pt;

 (*val nxt = Model_Problem ["normalize","polynomial","univariate","equation"]) *)

 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;

 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;

 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;

 val (p,_,f,nxt,_,pt) = me nxt p c pt;

 (*val nxt = Apply_Method ["PolyEq","normalize_poly"])     *)

 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;

 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;

 (*val nxt = Subproblem ("PolyEq",["polynomial","univariate","equation"]))*)

 if f = Form'

       (FormKF

          (~1,

             EdUndef,

             0,

             Nundef,

             "-16 * r ^^^ 4 + 8 * r ^^^ 2 * u ^^^ 2 = 0")) then ()

 else error "rlang.sml: diff.behav. in Schalk I s.87 Bsp 38b";

 val (p,_,f,nxt,_,pt) = me nxt p c pt;

 (*val nxt = Model_Problem ["sq_only","degree_2","polynomial","univariate","equation"]) *)

 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;

 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;

 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;

 val (p,_,f,nxt,_,pt) = me nxt p c pt;

 (*val nxt = Apply_Method ["PolyEq","solve_d2_polyeq_sqonly_equation"])     *)

 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;

 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;

 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;

 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;

 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;

 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;

 val (p,_,f,nxt,_,pt) = me nxt p c pt;

 if f = Form' (FormKF (~1,EdUndef,0,Nundef,"[u = sqrt (2 * r ^^^ 2 / 1), u = -1 * sqrt (2 * r ^^^ 2 / 1)]")) then()

 else error "rlang.sml WN.TEST new behaviour in max-rooteq";