(* Title:  Knowledge/polyeq-1.sml

            testexamples for PolyEq, poynomial equations and equational systems

    Author: Richard Lang 2003  

    (c) due to copyright terms

 Separation into polyeq-1.sml and polyeq-1a.sml due to 

 *)

 "-----------------------------------------------------------------";

 "table of contents -----------------------------------------------";

 "-----------------------------------------------------------------";

 "------ polyeq-1.sml ---------------------------------------------";

 "----------- tests on predicates in problems ---------------------";

 "----------- test matching problems ------------------------------";

 "----------- prep. for introduction of Matthias Goldgruber 2003 trials on rewrite orders -----";

 "----------- open local of fun ord_make_polynomial_in ------------------------------------------";

 "----------- Matthias Goldgruber 2003 trials on rewrite orders -------------------------------";

 "----------- lin.eq degree_0 -------------------------------------";

 "----------- test thm's d2_pq_formulsxx[_neg]---------------------";

 "----------- equality (2 +(- 1)*x + x \<up> 2 = (0::real)) ----------------------------------------";

 "----------- equality (- 2 +(- 1)*x + 1*x \<up> 2 = 0) ---------------------------------------------";

 "----------- equality (- 2 + x + x \<up> 2 = 0) ---------------------------------------------------";

 "----------- equality (2 + x + x \<up> 2 = 0) ----------------------------------------------------";

 "----------- equality (- 2 + x + 1*x \<up> 2 = 0)) ------------------------------------------------";

 "----------- equality (1*x +   x \<up> 2 = 0) ----------------------------------------------------";

 "----------- equality (1*x + 1*x \<up> 2 = 0) ----------------------------------------------------";

 "----------- equality (x +   x \<up> 2 = 0) ------------------------------------------------------";

 "----------- equality (x + 1*x \<up> 2 = 0) ------------------------------------------------------";

 "----------- equality (-4 + x \<up> 2 = 0) -------------------------------------------------------";

 "----------- equality (4 + 1*x \<up> 2 = 0) -------------------------------------------------------";

 "----------- equality (1 +(- 1)*x + 2*x \<up> 2 = 0) ----------------------------------------------";

 "----------- equality (- 1 + x + 2*x \<up> 2 = 0) -------------------------------------------------";

 "----------- equality (1 + x + 2*x \<up> 2 = 0) --------------------------------------------------";

 "----------- (-8 - 2*x + x \<up> 2 = 0),  (*Schalk 2, S.67 Nr.31.b----";

 "----------- (-8 - 2*x + x \<up> 2 = 0),  by rewriting ---------------";

 "----------- (- 16 + 4*x + 2*x \<up> 2 = 0), --------------------------";

 "-----------------------------------------------------------------";

 "------ polyeq-2.sml ---------------------------------------------";

 "----------- (a*b - (a+b)*x + x \<up> 2 = 0), (*Schalk 2,S.68Nr.44.a*)";

 "----------- (-64 + x \<up> 2 = 0), (*Schalk 2, S.66 Nr.1.a~--------*)";

 "----------- (- 147 + 3*x \<up> 2 = 0), (*Schalk 2, S.66 Nr.1.b------*)";

 "----------- (3*x - 1 - (5*x - (2 - 4*x)) = - 11),(*Schalk Is86Bsp5";

 "----------- ((x+1)*(x+2) - (3*x - 2) \<up> 2=.. Schalk II s.68 Bsp 37";

 "----------- rls make_polynomial_in ------------------------------";

 "----------- interSteps ([1],Res); on Schalk Is86Bsp5-------------";

 "----------- rls d2_polyeq_bdv_only_simplify ---------------------";

 "-----------------------------------------------------------------";

 "-----------------------------------------------------------------";

 \<close> ML \<open>

 Rewrite.trace_on := false (*false true*);

 "----------- tests on predicates in problems ---------------------";

 "----------- tests on predicates in problems ---------------------";

 "----------- tests on predicates in problems ---------------------";

 val thy = @{theory};

 Rewrite.trace_on:=false;  (*true false*)

  val t1 = (Thm.term_of o the o (TermC.parse thy)) "lhs (-8 - 2*x + x \<up> 2 = 0)";

  val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t1;

  if ((UnparseC.term t) = "- 8 - 2 * x + x \<up> 2") then ()

  else  error "polyeq.sml: diff.behav. in lhs";

 \<close> ML \<open>

  val t2 = (Thm.term_of o the o (TermC.parse thy)) "(-8 - 2*x + x \<up> 2) is_expanded_in x";

  val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t2;

  if (UnparseC.term t) = "True" then ()

  else  error "polyeq.sml: diff.behav. 1 in is_expended_in";

  val t0 = (Thm.term_of o the o (TermC.parse thy)) "(sqrt(x)) is_poly_in x";

  val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t0;

  if (UnparseC.term t) = "False" then ()

  else  error "polyeq.sml: diff.behav. 2 in is_poly_in";

  val t3 = (Thm.term_of o the o (TermC.parse thy)) "(-8 + (- 1)*2*x + x \<up> 2) is_poly_in x";

  val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t3;

  if (UnparseC.term t) = "True" then ()

  else  error "polyeq.sml: diff.behav. 3 in is_poly_in";

  val t4 = (Thm.term_of o the o (TermC.parse thy)) "(lhs (-8 + (- 1)*2*x + x \<up> 2 = 0)) is_expanded_in x";

  val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t4;

  if (UnparseC.term t) = "True" then ()

  else  error "polyeq.sml: diff.behav. 4 in is_expended_in";

  val t6 = (Thm.term_of o the o (TermC.parse thy)) "(lhs (-8 - 2*x + x \<up> 2 = 0)) is_expanded_in x";

  val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t6;

  if (UnparseC.term t) = "True" then ()

  else  error "polyeq.sml: diff.behav. 5 in is_expended_in";

  val t3 = (Thm.term_of o the o (TermC.parse thy))"((-8 - 2*x + x \<up> 2) has_degree_in x) = 2";

  val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t3;

  if (UnparseC.term t) = "True" then ()

  else  error "polyeq.sml: diff.behav. in has_degree_in_in";

  val t3 = (Thm.term_of o the o (TermC.parse thy)) "((sqrt(x)) has_degree_in x) = 2";

  val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t3;

  if (UnparseC.term t) = "False" then ()

  else  error "polyeq.sml: diff.behav. 6 in has_degree_in_in";

  val t4 = (Thm.term_of o the o (TermC.parse thy)) 

 	      "((-8 - 2*x + x \<up> 2) has_degree_in x) = 1";

  val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t4;

  if (UnparseC.term t) = "False" then ()

  else  error "polyeq.sml: diff.behav. 7 in has_degree_in_in";

 val t5 = (Thm.term_of o the o (TermC.parse thy)) 

 	      "((-8 - 2*x + x \<up> 2) has_degree_in x) = 2";

  val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t5;

  if (UnparseC.term t) = "True" then ()

  else  error "polyeq.sml: diff.behav. 8 in has_degree_in_in";

 \<close> ML \<open>

 "----------- test matching problems --------------------------0---";

 "----------- test matching problems --------------------------0---";

 "----------- test matching problems --------------------------0---";

 val fmz = ["equality (-8 - 2*x + x \<up> 2 = 0)", "solveFor x", "solutions L"];

 if M_Match.match_pbl fmz (Problem.from_store ["expanded", "univariate", "equation"]) =

   M_Match.Matches' {Find = [Correct "solutions L"], 

             With = [], 

             Given = [Correct "equality (- 8 - 2 * x + x \<up> 2 = 0)", Correct "solveFor x"], 

             Where = [Correct "matches (?a = 0) (- 8 - 2 * x + x \<up> 2 = 0)", 

                      Correct "lhs (- 8 - 2 * x + x \<up> 2 = 0) is_expanded_in x"], 

             Relate = []}

 then () else error "M_Match.match_pbl [expanded,univariate,equation]";

 if M_Match.match_pbl fmz (Problem.from_store ["degree_2", "expanded", "univariate", "equation"]) =

   M_Match.Matches' {Find = [Correct "solutions L"], 

             With = [], 

             Given = [Correct "equality (- 8 - 2 * x + x \<up> 2 = 0)", Correct "solveFor x"], 

             Where = [Correct "lhs (- 8 - 2 * x + x \<up> 2 = 0) has_degree_in x = 2"], 

             Relate = []}              (*before WN110906 was: has_degree_in x =!= 2"]*)

 then () else error "M_Match.match_pbl [degree_2,expanded,univariate,equation]";

 \<close> ML \<open>

 "----------- prep. for introduction of Matthias Goldgruber 2003 trials on rewrite orders -----";

 "----------- prep. for introduction of Matthias Goldgruber 2003 trials on rewrite orders -----";

 "----------- prep. for introduction of Matthias Goldgruber 2003 trials on rewrite orders -----";

 (*##################################################################################

 ----------- 28.2.03: war nicht upgedatet und ausgeklammert in ROOT.ML-->Test_Isac.thy

   (*Aufgabe zum Einstieg in die Arbeit...*)

   val t = (Thm.term_of o the o (TermC.parse thy)) "a*b - (a+b)*x + x \<up> 2 = 0";

   (*ein 'ruleset' aus Poly.ML wird angewandt...*)

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

   UnparseC.term t;

   "a * b + (- 1 * (a * x) + (- 1 * (b * x) + x \<up> 2)) = 0";

   val SOME (t,_) = 

       rewrite_set_inst_ thy Poly_erls false [("bdv", "a")] make_polynomial_in t;

   UnparseC.term t;

   "x \<up> 2 + (- 1 * (b * x) + (- 1 * (x * a) + b * a)) = 0";

 (* bei Verwendung von "size_of-term" nach MG :*)

 (*"x \<up> 2 + (- 1 * (b * x) + (b * a + - 1 * (x * a))) = 0"  !!! *)

   (*wir holen 'a' wieder aus der Klammerung heraus...*)

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

   UnparseC.term t;

    "x \<up> 2 + - 1 * b * x + - 1 * x * a + b * a = 0";

 (* "x \<up> 2 + - 1 * b * x + b * a + - 1 * x * a = 0" !!! *)

   val SOME (t,_) =

       rewrite_set_inst_ thy Poly_erls false [("bdv", "a")] make_polynomial_in t;

   UnparseC.term t;

   "x \<up> 2 + (- 1 * (b * x) + a * (b + - 1 * x)) = 0"; 

   (*da sind wir fast am Ziel: make_polynomial_in 'a' sollte ergeben

   "x \<up> 2 + (- 1 * (b * x)) + (b + - 1 * x) * a = 0"*)

   (*das rewriting l"asst sich beobachten mit

 Rewrite.trace_on := false; (*true false*)

   *)

 "------ 15.11.02 --------------------------";

   val t = (Thm.term_of o the o (TermC.parse thy)) "1 + a * x + b * x";

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

   val a = (Thm.term_of o the o (TermC.parse thy)) "a";

 Rewrite.trace_on := false; (*true false*)

  (* Anwenden einer Regelmenge aus Termorder.ML: *)

  val SOME (t,_) =

      rewrite_set_inst_ thy false [(bdv,a)] make_polynomial_in t;

  UnparseC.term t;

  val SOME (t,_) =

      rewrite_set_ thy false discard_parentheses t;

  UnparseC.term t;

 "1 + b * x + x * a";

  val t = (Thm.term_of o the o (TermC.parse thy)) "1 + a * (x + b * x) + a \<up> 2";

  val SOME (t,_) =

      rewrite_set_inst_ thy false [(bdv,a)] make_polynomial_in t;

  UnparseC.term t;

  val SOME (t,_) =

      rewrite_set_ thy false discard_parentheses t;

  UnparseC.term t;

 "1 + (x + b * x) * a + a \<up> 2";

  val t = (Thm.term_of o the o (TermC.parse thy)) "1 + a  \<up> 2 * x + b * a + 7*a \<up> 2";

  val SOME (t,_) =

      rewrite_set_inst_ thy false [(bdv,a)] make_polynomial_in t;

  UnparseC.term t;

  val SOME (t,_) =

      rewrite_set_ thy false discard_parentheses t;

  UnparseC.term t;

 "1 + b * a + (7 + x) * a \<up> 2";

 (* MG2003

  Prog_Expr.thy       grundlegende Algebra

  Poly.thy         Polynome

  Rational.thy     Br"uche

  Root.thy         Wurzeln

  RootRat.thy      Wurzen + Br"uche

  Termorder.thy    BITTE NUR HIERHER SCHREIBEN (...WN03)

  get_thm Termorder.thy "bdv_n_collect";

  get_thm (theory "Isac_Knowledge") "bdv_n_collect";

 *)

  val t = (Thm.term_of o the o (TermC.parse thy)) "a  \<up> 2 * x + 7 * a \<up> 2";

  val SOME (t,_) =

      rewrite_set_inst_ thy false [(bdv,a)] make_polynomial_in t;

  UnparseC.term t;

  val SOME (t,_) =

      rewrite_set_ thy false discard_parentheses t;

  UnparseC.term t;

 "(7 + x) * a \<up> 2";

  val t = (Thm.term_of o the o (TermC.parse Termorder.thy)) "Pi";

  val t = (Thm.term_of o the o (parseold thy)) "7";

 ##################################################################################*)

 \<close> ML \<open>

 "----------- open local of fun ord_make_polynomial_in ------------------------------------------";

 "----------- open local of fun ord_make_polynomial_in ------------------------------------------";

 "----------- open local of fun ord_make_polynomial_in ------------------------------------------";

 (* termorder hacked by MG, adapted later by WN *)

 (** )local ( *. for make_polynomial_in .*)

 open Term;  (* for type order = EQUAL | LESS | GREATER *)

 fun pr_ord EQUAL = "EQUAL"

   | pr_ord LESS  = "LESS"

   | pr_ord GREATER = "GREATER";

 fun dest_hd' _ (Const (a, T)) = (((a, 0), T), 0)

   | dest_hd' x (t as Free (a, T)) =

     if x = t then ((("|||||||||||||", 0), T), 0)                        (*WN*)

     else (((a, 0), T), 1)

   | dest_hd' _ (Var v) = (v, 2)

   | dest_hd' _ (Bound i) = ((("", i), dummyT), 3)

   | dest_hd' _ (Abs (_, T, _)) = ((("", 0), T), 4)

   | dest_hd' _ _ = raise ERROR "dest_hd': uncovered case in fun.def.";

 fun size_of_term' i pr x (t as Const (\<^const_name>\<open>realpow\<close>, _) $ 

       Free (var, _) $ Free (pot, _)) =

     (if pr then tracing (idt "#" i ^ "size_of_term' realpow: " ^ UnparseC.term t) else ();

     case x of                                                          (*WN*)

 	    (Free (xstr, _)) => 

 		    if xstr = var 

         then (if pr then tracing (idt "#" i ^ "xstr = var --> " ^ string_of_int (1000 * (the (TermC.int_opt_of_string pot)))) else ();

           1000 * (the (TermC.int_opt_of_string pot)))

         else (if pr then tracing (idt "#" i ^ "x <> Free  --> " ^ "3") else (); 3)

 	  | _ => raise ERROR ("size_of_term' called with subst = " ^ UnparseC.term x))

   | size_of_term' i pr x (t as Abs (_, _, body)) =

     (if pr then tracing (idt "#" i ^ "size_of_term' Abs: " ^ UnparseC.term t) else ();

     1 + size_of_term' (i + 1) pr x body)

   | size_of_term' i pr x (f $ t) =

     let

       val _ = if pr then tracing (idt "#" i ^ "size_of_term' $$$: " ^ UnparseC.term f ^ " $$$ " ^ UnparseC.term t) else ();

       val s1 = size_of_term' (i + 1) pr x f

       val s2 = size_of_term' (i + 1) pr x t

       val _ = if pr then tracing (idt "#" i ^ "size_of_term' $$$-->: " ^ string_of_int s1 ^ " + " ^ string_of_int s2 ^ " = " ^ string_of_int(s1 + s2)) else ();

     in (s1 + s2) end

   | size_of_term' i pr x t =

     (if pr then tracing (idt "#" i ^ "size_of_term' bot: " ^ UnparseC.term t) else ();

     case t of

       Free (subst, _) => 

        (case x of

    	     Free (xstr, _) =>

             if xstr = subst

             then (if pr then tracing (idt "#" i ^ "xstr = var --> " ^ "1000") else (); 1000)

             else (if pr then tracing (idt "#" i ^ "x <> Free  --> " ^ "1") else (); 1)

    	   | _ => raise ERROR ("size_of_term' called with subst = " ^ UnparseC.term x))

      | _ => (if pr then tracing (idt "#" i ^ "bot        --> " ^ "1") else (); 1));

 fun term_ord' i pr x thy (Abs (_, T, t), Abs(_, U, u)) =       (* ~ term.ML *)

     let

       val _ = if pr then tracing (idt "#" i ^ "term_ord' Abs") else ();

       val ord =

         case term_ord' (i + 1) pr x thy (t, u) of EQUAL => Term_Ord.typ_ord (T, U) | ord => ord

       val _  = if pr then tracing (idt "#" i ^ "term_ord' Abs --> " ^ pr_ord ord) else ()

     in ord end

   | term_ord' i pr x _ (t, u) =

     let

       val _ = if pr then tracing (idt "#" i ^ "term_ord' bot (" ^ UnparseC.term t ^ ", " ^ UnparseC.term u ^ ")") else ();

       val ord =

     	  case int_ord (size_of_term' (i + 1) pr x t, size_of_term' (i + 1) pr x u) of

     	    EQUAL =>

     	      let val (f, ts) = strip_comb t and (g, us) = strip_comb u 

             in

     	        (case hd_ord (i + 1) pr x (f, g) of 

     	           EQUAL => (terms_ord x (i + 1) pr) (ts, us) 

     	         | ord => ord)

     	      end

     	  | ord => ord

       val _  = if pr then tracing (idt "#" i ^ "term_ord' bot --> " ^ pr_ord ord) else ()

     in ord end

 and hd_ord i pr x (f, g) =                                        (* ~ term.ML *)

     let

       val _ = if pr then tracing (idt "#" i ^ "hd_ord (" ^ UnparseC.term f ^ ", " ^ UnparseC.term g ^ ")") else ();

       val ord = prod_ord

         (prod_ord Term_Ord.indexname_ord Term_Ord.typ_ord) int_ord

           (dest_hd' x f, dest_hd' x g)

       val _ = if pr then tracing (idt "#" i ^ "hd_ord --> " ^ pr_ord ord) else ();

     in ord end

 and terms_ord x i pr (ts, us) = 

     let

       val _ = if pr then tracing (idt "#" i ^ "terms_ord (" ^ UnparseC.terms ts ^ ", " ^ UnparseC.terms us ^ ")") else ();

       val ord = list_ord (term_ord' (i + 1) pr x (ThyC.get_theory "Isac_Knowledge"))(ts, us);

       val _ = if pr then tracing (idt "#" i ^ "terms_ord --> " ^ pr_ord ord) else ();

     in ord end

 (** )in( *local*)

 fun ord_make_polynomial_in (pr:bool) thy subst (ts, us) =

   ((** )tracing ("*** subs variable is: " ^ Env.subst2str subst); ( **)

 	case subst of

 	  (_, x) :: _ =>

       term_ord' 1 pr x thy (TermC.numerals_to_Free ts, TermC.numerals_to_Free us) = LESS

 	| _ => raise ERROR ("ord_make_polynomial_in called with subst = " ^ Env.subst2str subst))

 (** )end;( *local*)

 val subs = [(TermC.str2term "bdv::real", TermC.str2term "x::real")];

 if ord_make_polynomial_in false(*true*) @{theory} subs (t1, t2) then ()  else error "still GREATER?";

 val x = TermC.str2term "x ::real";

 val t1 = TermC.numerals_to_Free (TermC.str2term "L * q_0 * x \<up> 2 / 4 ::real");

 if 2006 = size_of_term' 1 false(*true*) x t1 

 then () else error "size_of_term' (L * q_0 * x \<up> 2) CHANGED)";

 val t2 = TermC.numerals_to_Free (TermC.str2term "- 1 * (q_0 * x \<up> 3) :: real");

 if 3004 = size_of_term' 1 false(*true*) x t2

 then () else error "size_of_term' (- 1 * (q_0 * x \<up> 3)) CHANGED";

 \<close> ML \<open>

 "----------- Matthias Goldgruber 2003 trials on rewrite orders -------------------------------";

 "----------- Matthias Goldgruber 2003 trials on rewrite orders -------------------------------";

 "----------- Matthias Goldgruber 2003 trials on rewrite orders -------------------------------";

   val substa = [(TermC.empty, (Thm.term_of o the o (TermC.parse thy)) "a")];

   val substb = [(TermC.empty, (Thm.term_of o the o (TermC.parse thy)) "b")];

   val substx = [(TermC.empty, (Thm.term_of o the o (TermC.parse thy)) "x")];

   val x1 = (Thm.term_of o the o (TermC.parse thy)) "a + b + x";

   val x2 = (Thm.term_of o the o (TermC.parse thy)) "a + x + b";

   val x3 = (Thm.term_of o the o (TermC.parse thy)) "a + x + b";

   val x4 = (Thm.term_of o the o (TermC.parse thy)) "x + a + b";

 if ord_make_polynomial_in false(*true*) thy substx (x1,x2) = true(*LESS *) then ()

 else error "termorder.sml diff.behav ord_make_polynomial_in #1";

 if ord_make_polynomial_in false(*true*) thy substa (x1,x2) = true(*LESS *) then ()

 else error "termorder.sml diff.behav ord_make_polynomial_in #2";

 if ord_make_polynomial_in false(*true*) thy substb (x1,x2) = false(*GREATER*) then ()

 else error "termorder.sml diff.behav ord_make_polynomial_in #3";

   val aa = (Thm.term_of o the o (TermC.parse thy)) "- 1 * a * x";

   val bb = (Thm.term_of o the o (TermC.parse thy)) "x \<up> 3";

   ord_make_polynomial_in false(*true*) thy substx (aa, bb);

   true; (* => LESS *) 

   val aa = (Thm.term_of o the o (TermC.parse thy)) "- 1 * a * x";

   val bb = (Thm.term_of o the o (TermC.parse thy)) "x \<up> 3";

   ord_make_polynomial_in false(*true*) thy substa (aa, bb);

   false; (* => GREATER *)

 (* und nach dem Re-engineering der Termorders in den 'rulesets' 

    kannst Du die 'gr"osste' Variable frei w"ahlen: *)

   val bdv= TermC.str2term "bdv ::real";

   val x  = TermC.str2term "x ::real";

   val a  = TermC.str2term "a ::real";

   val b  = TermC.str2term "b ::real";

 val SOME (t',_) = rewrite_set_inst_ thy false [(bdv,a)] make_polynomial_in x2;

 if UnparseC.term t' = "b + x + a" then ()

 else error "termorder.sml diff.behav ord_make_polynomial_in #11";

 val NONE = rewrite_set_inst_ thy false [(bdv,b)] make_polynomial_in x2;

 val SOME (t',_) = rewrite_set_inst_ thy false [(bdv,x)] make_polynomial_in x2;

 if UnparseC.term t' = "a + b + x" then ()

 else error "termorder.sml diff.behav ord_make_polynomial_in #13";

   val ppp' = "-6 + -5*x + x \<up> 3 + - 1*x \<up> 2 + - 1*x \<up> 3 + - 14*x \<up> 2";

   val ppp  = (Thm.term_of o the o (TermC.parse thy)) ppp';

 val SOME (t', _) = rewrite_set_inst_ thy false [(bdv,x)] make_polynomial_in ppp;

 if UnparseC.term t' = "- 6 + - 5 * x + - 15 * x \<up> 2" then ()

 else error "termorder.sml diff.behav ord_make_polynomial_in #15";

   val ttt' = "(3*x + 5)/18 ::real";

   val ttt = (Thm.term_of o the o (TermC.parse thy)) ttt';

 val SOME (uuu,_) = rewrite_set_inst_ thy false [(bdv,x)] make_polynomial_in ttt;

 if UnparseC.term uuu = "(5 + 3 * x) / 18" then ()

 else error "termorder.sml diff.behav ord_make_polynomial_in #16a";

 val SOME (uuu,_) = rewrite_set_ thy false make_polynomial ttt;

 if UnparseC.term uuu = "(5 + 3 * x) / 18" then ()

 else error "termorder.sml diff.behav ord_make_polynomial_in #16b";

 \<close> ML \<open>

 "----------- lin.eq degree_0 -------------------------------------";

 "----------- lin.eq degree_0 -------------------------------------";

 "----------- lin.eq degree_0 -------------------------------------";

 "----- d0_false ------";

 val fmz = ["equality (1 = (0::real))", "solveFor x", "solutions L"];

 val (dI',pI',mI') = ("PolyEq",["degree_0", "polynomial", "univariate", "equation"],

                      ["PolyEq", "solve_d0_polyeq_equation"]);

 (*=== inhibit exn WN110914: declare_constraints doesnt work with ThmC.numerals_to_Free ========

 TODO: change to "equality (x + - 1*x = (0::real))"

       and search for an appropriate problem and method.

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

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

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

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

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

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

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

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

 	 | _ => error "polyeq.sml: diff.behav. in 1 = 0 -> []";

 "----- d0_true ------";

 val fmz = ["equality (0 = (0::real))", "solveFor x", "solutions L"];

 val (dI',pI',mI') = ("PolyEq",["degree_0", "polynomial", "univariate", "equation"],

                      ["PolyEq", "solve_d0_polyeq_equation"]);

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

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

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

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

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

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

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

 case f of Form' (Test_Out.FormKF (~1,EdUndef,0,Nundef,"UniversalList")) => ()

 	 | _ => error "polyeq.sml: diff.behav. in 0 = 0 -> UniversalList";

 ============ inhibit exn WN110914 ============================================*)

 \<close> text \<open> (*=====calcul: rhs = (- 1) \<up> 2 *)

 "----------- test thm's d2_pq_formulsxx[_neg]---------------------";

 "----------- test thm's d2_pq_formulsxx[_neg]---------------------";

 "----------- test thm's d2_pq_formulsxx[_neg]---------------------";

 "----- d2_pqformula1 ------!!!!";

 val fmz = ["equality (- 1/8 + (- 1/4)*z + z \<up> 2 = (0::real))", "solveFor z", "solutions L"];

 val (dI',pI',mI') =

   ("Isac_Knowledge", ["pqFormula", "degree_2", "polynomial", "univariate", "equation"], ["no_met"]);

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

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

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

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

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

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

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

 val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*Apply_Method ["PolyEq", "solve_d2_polyeq_pq_equation"]*)

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

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

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

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

 (*[z = 1 / 8 + sqrt (9 / 16) / 2, z = 1 / 8 + - 1 * sqrt (9 / 16) / 2] TODO sqrt*)

 val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt =..,Check_elementwise "Assumptions")*)

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

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

 if p = ([], Res) andalso

   f2str f = "[z = 1 / 8 + sqrt (9 / 16) / 2, z = 1 / 8 + - 1 * sqrt (9 / 16) / 2]" then

     case nxt of End_Proof' => () | _ => error "(- 1/8 + (- 1/4)*z + z \<up> 2 = (0::real)) CHANGED 1"

 else error "(- 1/8 + (- 1/4)*z + z \<up> 2 = (0::real)) CHANGED 2";

 \<close> text \<open> (*=====calcul: rhs = (- 1) \<up> 2 *)

 "----------- equality (2 +(- 1)*x + x \<up> 2 = (0::real)) ----------------------------------------";

 "----------- equality (2 +(- 1)*x + x \<up> 2 = (0::real)) ----------------------------------------";

 "----------- equality (2 +(- 1)*x + x \<up> 2 = (0::real)) ----------------------------------------";

 "----- d2_pqformula1_neg ------";

 val fmz = ["equality (2 +(- 1)*x + x \<up> 2 = (0::real))", "solveFor x", "solutions L"];

 val (dI',pI',mI') = ("PolyEq",["pqFormula", "degree_2", "polynomial", "univariate", "equation"], ["PolyEq", "solve_d2_polyeq_pq_equation"]);

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

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

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

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

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

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

 (*### or2list False

   ([1],Res)  False   Or_to_List)*)

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

 (*### or2list False                           

   ([2],Res)  []      Check_elementwise "Assumptions"*)

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

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

 val asm = Ctree.get_assumptions pt p;

 if f2str f = "[]" andalso 

   UnparseC.terms asm = "[\"lhs (2 + - 1 * x + x \<up> 2 = 0) is_poly_in x\", " ^

     "\"lhs (2 + - 1 * x + x \<up> 2 = 0) has_degree_in x = 2\"]" then ()

 else error "polyeq.sml: diff.behav. in 2 +(- 1)*x + x \<up> 2 = 0";

 \<close> text \<open> (*=====calcul: rhs = (- 1) \<up> 2 *)

 "----------- equality (- 2 +(- 1)*x + 1*x \<up> 2 = 0) ---------------------------------------------";

 "----------- equality (- 2 +(- 1)*x + 1*x \<up> 2 = 0) ---------------------------------------------";

 "----------- equality (- 2 +(- 1)*x + 1*x \<up> 2 = 0) ---------------------------------------------";

 "----- d2_pqformula2 ------";

 val fmz = ["equality (- 2 +(- 1)*x + 1*x \<up> 2 = 0)", "solveFor x", "solutions L"];

 val (dI',pI',mI') = ("PolyEq",["pqFormula", "degree_2", "polynomial", "univariate", "equation"],

                      ["PolyEq", "solve_d2_polyeq_pq_equation"]);

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

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

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

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

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

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

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

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

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

 case f of Test_Out.FormKF "[x = 2, x = - 1]" => ()

 	 | _ => error "polyeq.sml: diff.behav. in - 2 + (- 1)*x + x^2 = 0 -> [x = 2, x = - 1]";

 \<close> ML \<open>

 "----------- equality (- 2 + x + x \<up> 2 = 0) ---------------------------------------------------";

 "----------- equality (- 2 + x + x \<up> 2 = 0) ---------------------------------------------------";

 "----------- equality (- 2 + x + x \<up> 2 = 0) ---------------------------------------------------";

 "----- d2_pqformula3 ------";

 (*EP-9*)

 val fmz = ["equality (- 2 + x + x \<up> 2 = 0)", "solveFor x", "solutions L"];

 val (dI',pI',mI') = ("PolyEq",["pqFormula", "degree_2", "polynomial", "univariate", "equation"],

                      ["PolyEq", "solve_d2_polyeq_pq_equation"]);

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

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

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

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

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

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

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

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

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

 case f of Test_Out.FormKF "[x = 1, x = - 2]" => ()

 	 | _ => error "polyeq.sml: diff.behav. in  - 2 + x + x^2 = 0-> [x = 1, x = - 2]";

 \<close> ML \<open>

 "----------- equality (2 + x + x \<up> 2 = 0) ----------------------------------------------------";

 "----------- equality (2 + x + x \<up> 2 = 0) ----------------------------------------------------";

 "----------- equality (2 + x + x \<up> 2 = 0) ----------------------------------------------------";

 "----- d2_pqformula3_neg ------";

 val fmz = ["equality (2 + x + x \<up> 2 = 0)", "solveFor x", "solutions L"];

 val (dI',pI',mI') = ("PolyEq",["pqFormula", "degree_2", "polynomial", "univariate", "equation"],

                      ["PolyEq", "solve_d2_polyeq_pq_equation"]);

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

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

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

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

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

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

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

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

 "TODO 2 + x + x \<up> 2 = 0";

 "TODO 2 + x + x \<up> 2 = 0";

 "TODO 2 + x + x \<up> 2 = 0";

 \<close> ML \<open>

 "----------- equality (- 2 + x + 1*x \<up> 2 = 0)) ------------------------------------------------";

 "----------- equality (- 2 + x + 1*x \<up> 2 = 0)) ------------------------------------------------";

 "----------- equality (- 2 + x + 1*x \<up> 2 = 0)) ------------------------------------------------";

 "----- d2_pqformula4 ------";

 val fmz = ["equality (- 2 + x + 1*x \<up> 2 = 0)", "solveFor x", "solutions L"];

 val (dI',pI',mI') = ("PolyEq",["pqFormula", "degree_2", "polynomial", "univariate", "equation"],

                      ["PolyEq", "solve_d2_polyeq_pq_equation"]);

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

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

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

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

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

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

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

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

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

 case f of Test_Out.FormKF "[x = 1, x = - 2]" => ()

 	 | _ => error "polyeq.sml: diff.behav. in  - 2 + x + 1*x \<up> 2 = 0 -> [x = 1, x = - 2]";

 \<close> ML \<open>

 "----------- equality (1*x +   x \<up> 2 = 0) ----------------------------------------------------";

 "----------- equality (1*x +   x \<up> 2 = 0) ----------------------------------------------------";

 "----------- equality (1*x +   x \<up> 2 = 0) ----------------------------------------------------";

 "----- d2_pqformula5 ------";

 val fmz = ["equality (1*x +   x \<up> 2 = 0)", "solveFor x", "solutions L"];

 val (dI',pI',mI') = ("PolyEq",["pqFormula", "degree_2", "polynomial", "univariate", "equation"],

                      ["PolyEq", "solve_d2_polyeq_pq_equation"]);

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

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

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

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

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

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

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

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

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

 case f of Test_Out.FormKF "[x = 0, x = - 1]" => ()

 	 | _ => error "polyeq.sml: diff.behav. in  1*x +   x^2 = 0 -> [x = 0, x = - 1]";

 \<close> ML \<open>

 "----------- equality (1*x + 1*x \<up> 2 = 0) ----------------------------------------------------";

 "----------- equality (1*x + 1*x \<up> 2 = 0) ----------------------------------------------------";

 "----------- equality (1*x + 1*x \<up> 2 = 0) ----------------------------------------------------";

 "----- d2_pqformula6 ------";

 val fmz = ["equality (1*x + 1*x \<up> 2 = 0)", "solveFor x", "solutions L"];

 val (dI',pI',mI') = ("PolyEq",["pqFormula", "degree_2", "polynomial", "univariate", "equation"],

                      ["PolyEq", "solve_d2_polyeq_pq_equation"]);

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

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

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

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

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

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

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

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

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

 case f of Test_Out.FormKF "[x = 0, x = - 1]" => ()

 	 | _ => error "polyeq.sml: diff.behav. in  1*x + 1*x^2 = 0 -> [x = 0, x = - 1]";

 \<close> ML \<open> (*=====calcul: rhs = (1::?'a) - (0::?'a) *)

 "----------- equality (x +   x \<up> 2 = 0) ------------------------------------------------------";

 "----------- equality (x +   x \<up> 2 = 0) ------------------------------------------------------";

 "----------- equality (x +   x \<up> 2 = 0) ------------------------------------------------------";

 "----- d2_pqformula7 ------";

 (*EP- 10*)

 val fmz = ["equality (  x +   x \<up> 2 = (0::real))", "solveFor x", "solutions L"];

 val (dI',pI',mI') = ("PolyEq",["pqFormula", "degree_2", "polynomial", "univariate", "equation"],

                      ["PolyEq", "solve_d2_polyeq_pq_equation"]);

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

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

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

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

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

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

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

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

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

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

 case f of Test_Out.FormKF "[x = 0, x = - 1]" => ()

 	 | _ => error "polyeq.sml: diff.behav. in  x + x^2 = 0 -> [x = 0, x = - 1]";

 \<close> ML \<open> (*=====calcul: rhs = (1::?'b) - (0::?'b) *)

 "----------- equality (x + 1*x \<up> 2 = 0) ------------------------------------------------------";

 "----------- equality (x + 1*x \<up> 2 = 0) ------------------------------------------------------";

 "----------- equality (x + 1*x \<up> 2 = 0) ------------------------------------------------------";

 "----- d2_pqformula8 ------";

 val fmz = ["equality (x + 1*x \<up> 2 = 0)", "solveFor x", "solutions L"];

 val (dI',pI',mI') = ("PolyEq",["pqFormula", "degree_2", "polynomial", "univariate", "equation"],

                      ["PolyEq", "solve_d2_polyeq_pq_equation"]);

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

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

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

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

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

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

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

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

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

 case f of Test_Out.FormKF "[x = 0, x = - 1]" => ()

 	 | _ => error "polyeq.sml: diff.behav. in  x + 1*x^2 = 0 -> [x = 0, x = - 1]";

 \<close> ML \<open>

 "----------- equality (-4 + x \<up> 2 = 0) -------------------------------------------------------";

 "----------- equality (-4 + x \<up> 2 = 0) -------------------------------------------------------";

 "----------- equality (-4 + x \<up> 2 = 0) -------------------------------------------------------";

 "----- d2_pqformula9 ------";

 val fmz = ["equality (-4 + x \<up> 2 = 0)", "solveFor x", "solutions L"];

 val (dI',pI',mI') = ("PolyEq",["pqFormula", "degree_2", "polynomial", "univariate", "equation"],

                      ["PolyEq", "solve_d2_polyeq_pq_equation"]);

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

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

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

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

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

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

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

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

 case f of Test_Out.FormKF "[x = 2, x = - 2]" => ()

 	 | _ => error "polyeq.sml: diff.behav. in -4 + x^2 = 0 -> [x = 2, x = - 2]";

 \<close> ML \<open>

 "----------- equality (4 + 1*x \<up> 2 = 0) -------------------------------------------------------";

 "----------- equality (4 + 1*x \<up> 2 = 0) -------------------------------------------------------";

 "----------- equality (4 + 1*x \<up> 2 = 0) -------------------------------------------------------";

 "----- d2_pqformula9_neg ------";

 val fmz = ["equality (4 + 1*x \<up> 2 = 0)", "solveFor x", "solutions L"];

 val (dI',pI',mI') = ("PolyEq",["pqFormula", "degree_2", "polynomial", "univariate", "equation"],

                      ["PolyEq", "solve_d2_polyeq_pq_equation"]);

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

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

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

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

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

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

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

 "TODO 4 + 1*x \<up> 2 = 0";

 "TODO 4 + 1*x \<up> 2 = 0";

 "TODO 4 + 1*x \<up> 2 = 0";

 \<close> text \<open> (*=====calcul: rhs = (- 1) \<up> 2 *)

 "-------------------- test thm's d2_abc_formulsxx[_neg]-----";

 "-------------------- test thm's d2_abc_formulsxx[_neg]-----";

 "-------------------- test thm's d2_abc_formulsxx[_neg]-----";

 val fmz = ["equality (- 1 +(- 1)*x + 2*x \<up> 2 = 0)", "solveFor x", "solutions L"];

 val (dI',pI',mI') = ("PolyEq",["abcFormula", "degree_2", "polynomial", "univariate", "equation"],

                      ["PolyEq", "solve_d2_polyeq_abc_equation"]);

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

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

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

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

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

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

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

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

 case f of Test_Out.FormKF "[x = 1, x = - 1 / 2]" => ()

 	 | _ => error "polyeq.sml: diff.behav. in - 1 + (- 1)*x + 2*x^2 = 0 -> [x = 1, x = - 1/2]";

 \<close> text \<open> (*=====calcul: rhs = (- 1) \<up> 2 *)

 "----------- equality (1 +(- 1)*x + 2*x \<up> 2 = 0) ----------------------------------------------";

 "----------- equality (1 +(- 1)*x + 2*x \<up> 2 = 0) ----------------------------------------------";

 "----------- equality (1 +(- 1)*x + 2*x \<up> 2 = 0) ----------------------------------------------";

 val fmz = ["equality (1 +(- 1)*x + 2*x \<up> 2 = 0)", "solveFor x", "solutions L"];

 val (dI',pI',mI') = ("PolyEq",["abcFormula", "degree_2", "polynomial", "univariate", "equation"],

                      ["PolyEq", "solve_d2_polyeq_abc_equation"]);

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

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

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

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

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

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

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

 "TODO 1 +(- 1)*x + 2*x \<up> 2 = 0";

 "TODO 1 +(- 1)*x + 2*x \<up> 2 = 0";

 "TODO 1 +(- 1)*x + 2*x \<up> 2 = 0";

 \<close> ML \<open>

 "----------- equality (- 1 + x + 2*x \<up> 2 = 0) -------------------------------------------------";

 "----------- equality (- 1 + x + 2*x \<up> 2 = 0) -------------------------------------------------";

 "----------- equality (- 1 + x + 2*x \<up> 2 = 0) -------------------------------------------------";

 (*EP- 11*)

 val fmz = ["equality (- 1 + x + 2*x \<up> 2 = 0)", "solveFor x", "solutions L"];

 val (dI',pI',mI') = ("PolyEq",["abcFormula", "degree_2", "polynomial", "univariate", "equation"],

                      ["PolyEq", "solve_d2_polyeq_abc_equation"]);

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

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

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

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

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

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

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

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

 case f of Test_Out.FormKF "[x = 1 / 2, x = - 1]" => ()

 	 | _ => error "polyeq.sml: diff.behav. in - 1 + x + 2*x^2 = 0 -> [x = 1/2, x = - 1]";

 \<close> text \<open> (*=====calcul: rhs = (1::?'c) - (0::?'c) *)

 "----------- equality (1 + x + 2*x \<up> 2 = 0) --------------------------------------------------";

 "----------- equality (1 + x + 2*x \<up> 2 = 0) --------------------------------------------------";

 "----------- equality (1 + x + 2*x \<up> 2 = 0) --------------------------------------------------";

 val fmz = ["equality (1 + x + 2*x \<up> 2 = 0)", "solveFor x", "solutions L"];

 val (dI',pI',mI') = ("PolyEq",["abcFormula", "degree_2", "polynomial", "univariate", "equation"],

                      ["PolyEq", "solve_d2_polyeq_abc_equation"]);

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

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

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

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

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

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

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

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

 "TODO 1 + x + 2*x \<up> 2 = 0";

 "TODO 1 + x + 2*x \<up> 2 = 0";

 "TODO 1 + x + 2*x \<up> 2 = 0";

 val fmz = ["equality (- 2 + 1*x + x \<up> 2 = 0)", "solveFor x", "solutions L"];

 val (dI',pI',mI') = ("PolyEq",["abcFormula", "degree_2", "polynomial", "univariate", "equation"],

                      ["PolyEq", "solve_d2_polyeq_abc_equation"]);

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

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

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

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

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

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

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

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

 case f of Test_Out.FormKF "[x = 1, x = - 2]" => ()

 	 | _ => error "polyeq.sml: diff.behav. in - 2 + 1*x + x^2 = 0 -> [x = 1, x = - 2]";

 val fmz = ["equality ( 2 + 1*x + x \<up> 2 = 0)", "solveFor x", "solutions L"];

 val (dI',pI',mI') = ("PolyEq",["abcFormula", "degree_2", "polynomial", "univariate", "equation"],

                      ["PolyEq", "solve_d2_polyeq_abc_equation"]);

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

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

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

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

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

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

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

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

 "TODO 2 + 1*x + x \<up> 2 = 0";

 "TODO 2 + 1*x + x \<up> 2 = 0";

 "TODO 2 + 1*x + x \<up> 2 = 0";

 (*EP- 12*)

 val fmz = ["equality (- 2 + x + x \<up> 2 = 0)", "solveFor x", "solutions L"];

 val (dI',pI',mI') = ("PolyEq",["abcFormula", "degree_2", "polynomial", "univariate", "equation"],

                      ["PolyEq", "solve_d2_polyeq_abc_equation"]);

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

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

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

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

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

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

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

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

 case f of Test_Out.FormKF "[x = 1, x = - 2]" => ()

 	 | _ => error "polyeq.sml: diff.behav. in - 2 + x + x^2 = 0 -> [x = 1, x = - 2]";

 val fmz = ["equality ( 2 + x + x \<up> 2 = 0)", "solveFor x", "solutions L"];

 val (dI',pI',mI') = ("PolyEq",["abcFormula", "degree_2", "polynomial", "univariate", "equation"],

                      ["PolyEq", "solve_d2_polyeq_abc_equation"]);

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

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

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

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

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

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

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

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

 "TODO 2 + x + x \<up> 2 = 0";

 "TODO 2 + x + x \<up> 2 = 0";

 "TODO 2 + x + x \<up> 2 = 0";

 (*EP- 13*)

 val fmz = ["equality (-8 + 2*x \<up> 2 = 0)", "solveFor x", "solutions L"];

 val (dI',pI',mI') = ("PolyEq",["abcFormula", "degree_2", "polynomial", "univariate", "equation"],

                      ["PolyEq", "solve_d2_polyeq_abc_equation"]);

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

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

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

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

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

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

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

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

 case f of Test_Out.FormKF "[x = 2, x = - 2]" => ()

 	 | _ => error "polyeq.sml: diff.behav. in -8 + 2*x^2 = 0 -> [x = 2, x = - 2]";

 val fmz = ["equality ( 8+ 2*x \<up> 2 = 0)", "solveFor x", "solutions L"];

 val (dI',pI',mI') = ("PolyEq",["abcFormula", "degree_2", "polynomial", "univariate", "equation"],

                      ["PolyEq", "solve_d2_polyeq_abc_equation"]);

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

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

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

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

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

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

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

 "TODO 8+ 2*x \<up> 2 = 0";

 "TODO 8+ 2*x \<up> 2 = 0";

 "TODO 8+ 2*x \<up> 2 = 0";

 (*EP- 14*)

 val fmz = ["equality (-4 + x \<up> 2 = 0)", "solveFor x", "solutions L"];

 val (dI',pI',mI') = ("PolyEq",["abcFormula", "degree_2", "polynomial", "univariate", "equation"], ["PolyEq", "solve_d2_polyeq_abc_equation"]);

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

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

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

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

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

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

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

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

 case f of Test_Out.FormKF "[x = 2, x = - 2]" => ()

 	 | _ => error "polyeq.sml: diff.behav. in -4 + x^2 = 0 -> [x = 2, x = - 2]";

 val fmz = ["equality ( 4+ x \<up> 2 = 0)", "solveFor x", "solutions L"];

 val (dI',pI',mI') = ("PolyEq",["abcFormula", "degree_2", "polynomial", "univariate", "equation"], ["PolyEq", "solve_d2_polyeq_abc_equation"]);

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

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

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

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

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

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

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

 "TODO 4+ x \<up> 2 = 0";

 "TODO 4+ x \<up> 2 = 0";

 "TODO 4+ x \<up> 2 = 0";

 (*EP- 15*)

 val fmz = ["equality (2*x + 2*x \<up> 2 = 0)", "solveFor x", "solutions L"];

 val (dI',pI',mI') = ("PolyEq",["abcFormula", "degree_2", "polynomial", "univariate", "equation"],

                      ["PolyEq", "solve_d2_polyeq_abc_equation"]);

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

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

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

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

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

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

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

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

 case f of Test_Out.FormKF "[x = 0, x = - 1]" => ()

 	 | _ => error "polyeq.sml: diff.behav. in x + x^2 = 0 -> [x = 0, x = - 1]";

 val fmz = ["equality (1*x + x \<up> 2 = 0)", "solveFor x", "solutions L"];

 val (dI',pI',mI') = ("PolyEq",["abcFormula", "degree_2", "polynomial", "univariate", "equation"],

                      ["PolyEq", "solve_d2_polyeq_abc_equation"]);

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

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

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

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

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

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

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

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

 case f of Test_Out.FormKF "[x = 0, x = - 1]" => ()

 	 | _ => error "polyeq.sml: diff.behav. in x + x^2 = 0 -> [x = 0, x = - 1]";

 (*EP- 16*)

 val fmz = ["equality (x + 2 * x \<up> 2 = (0::real))", "solveFor (x::real)", "solutions L"];

 val (dI',pI',mI') = ("PolyEq",["abcFormula", "degree_2", "polynomial", "univariate", "equation"],

                      ["PolyEq", "solve_d2_polyeq_abc_equation"]);

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

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

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

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

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

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

 (*+*)val Test_Out.FormKF "x + 2 * x \<up> 2 = 0" = f;

 (*+*)val Rewrite_Set_Inst (["(''bdv'', x)"], "d2_polyeq_abcFormula_simplify") = nxt

 val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*"x + 2 * x \<up> 2 = 0", d2_polyeq_abcFormula_simplify*)

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

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

 case f of Test_Out.FormKF "[x = 0, x = - 1 / 2]" => ()

 	 | _ => error "polyeq.sml: diff.behav. in x + x^2 = 0 -> [x = 0, x = - 1 / 2]";

 (*EP-//*)

 val fmz = ["equality (x + x \<up> 2 = 0)", "solveFor x", "solutions L"];

 val (dI',pI',mI') = ("PolyEq",["abcFormula", "degree_2", "polynomial", "univariate", "equation"],

                      ["PolyEq", "solve_d2_polyeq_abc_equation"]);

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

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

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

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

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

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

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

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

 case f of Test_Out.FormKF "[x = 0, x = - 1]" => ()

 	 | _ => error "polyeq.sml: diff.behav. in x + x^2 = 0 -> [x = 0, x = - 1]";

 \<close> ML \<open>

 "----------- (-8 - 2*x + x \<up> 2 = 0),  (*Schalk 2, S.67 Nr.31.b----";

 "----------- (-8 - 2*x + x \<up> 2 = 0),  (*Schalk 2, S.67 Nr.31.b----";

 "----------- (-8 - 2*x + x \<up> 2 = 0),  (*Schalk 2, S.67 Nr.31.b----";

 (*stopped du to TODO.txt WN111014.TODO calculate_Poly < calculate_Rational < calculate_RootRat

 see --- val rls = calculate_RootRat > calculate_Rational ---

 calculate_RootRat was a TODO with 2002, requires re-design.

 see also --- (-8 - 2*x + x \<up> 2 = 0),  by rewriting --- below

 *)

  val fmz = ["equality (-8 - 2*x + x \<up> 2 = 0)", (*Schalk 2, S.67 Nr.31.b*)

  	    "solveFor x", "solutions L"];

  val (dI',pI',mI') =

      ("PolyEq",["degree_2", "expanded", "univariate", "equation"],

       ["PolyEq", "complete_square"]);

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

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

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

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

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

 (*Apply_Method ("PolyEq", "complete_square")*)

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

 (*"-8 - 2 * x + x \<up> 2 = 0", nxt = Rewrite_Set_Inst ... "complete_square*)

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

 (*"-8 + (2 / 2 - x) \<up> 2 = (2 / 2) \<up> 2", nxt = Rewrite("square_explicit1"*)

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

 (*"(2 / 2 - x) \<up> 2 = (2 / 2) \<up> 2 - -8" nxt = Rewrite("root_plus_minus*)

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

 (*"2 / 2 - x = sqrt ((2 / 2) \<up> 2 - -8) |

    2 / 2 - x = - sqrt ((2 / 2) \<up> 2 - -8)" nxt = Rewr_Inst("bdv_explicit2"*)

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

 (*"2 / 2 - x = sqrt ((2 / 2) \<up> 2 - -8) |

    - 1*x = - (2 / 2) + - sqrt ((2 / 2) \<up> 2 - -8)"nxt = R_Inst("bdv_explt2"*)

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

 (*"- 1 * x = - (2 / 2) + sqrt ((2 / 2) \<up> 2 - -8) |

    - 1 * x = (- (2 / 2) + - sqrt ((2 / 2) \<up> 2 - -8))"nxt = bdv_explicit3*)

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

 (*"- 1 * x = - (2 / 2) + sqrt ((2 / 2) \<up> 2 - -8) |

   x = - 1 * (- (2 / 2) + - sqrt ((2 / 2) \<up> 2 - -8))" nxt = bdv_explicit3*)

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

 (*"x = - 1 * (- (2 / 2) + sqrt ((2 / 2) \<up> 2 - -8)) |

    x = - 1 * (- (2 / 2) + - sqrt ((2 / 2) \<up> 2 - -8))"nxt = calculate_Rational

    NOT IMPLEMENTED SINCE 2002 ------------------------------ \<up> \<up> \<up> \<up> \<up>  \<up> *)

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

 (*"x = - 2 | x = 4" nxt = Or_to_List*)

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

 (*"[x = - 2, x = 4]" nxt = Check_Postcond*)

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

 (* FIXXXME 

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

 	 | _ => error "polyeq.sml: diff.behav. in [x = - 2, x = 4]";

 *)

 if f2str f =

    "[x = - 1 * - 1 + - 1 * sqrt (2 \<up> 2 / 2 \<up> 2 - - 8),\n x = - 1 * - 1 + - 1 * (- 1 * sqrt (2 \<up> 2 / 2 \<up> 2 - - 8))]"

 (*"[x = - 1 * - 1 + - 1 * sqrt (1 \<up> 2 - -8),\n x = - 1 * - 1 + - 1 * (- 1 * sqrt (1 \<up> 2 - -8))]"*)

 then () else error "polyeq.sml corrected?behav. in [x = - 2, x = 4]";

 "----------- (-8 - 2*x + x \<up> 2 = 0),  by rewriting ---------------";

 "----------- (-8 - 2*x + x \<up> 2 = 0),  by rewriting ---------------";

 "----------- (-8 - 2*x + x \<up> 2 = 0),  by rewriting ---------------";

 (*stopped due to TODO.txt WN111014.TODO calculate_Poly < calculate_Rational < calculate_RootRat

 see --- val rls = calculate_RootRat > calculate_Rational ---*)

 val thy = @{theory PolyEq};

 val ctxt = Proof_Context.init_global thy;

 val inst = [((the o (parseNEW  ctxt)) "bdv::real", (the o (parseNEW  ctxt)) "x::real")];

 val t = (the o (parseNEW  ctxt)) "-8 - 2*x + x \<up> 2 = (0::real)";

 val rls = complete_square;

 val SOME (t,asm) = rewrite_set_inst_ thy true inst rls t;

 if UnparseC.term t = "- 8 + (2 / 2 - x) \<up> 2 = (2 / 2) \<up> 2"

 then () else error "rls complete_square CHANGED";

 val thm = @{thm square_explicit1};

 val SOME (t,asm) = rewrite_ thy dummy_ord Rule_Set.Empty true thm t;

 if UnparseC.term t = "(2 / 2 - x) \<up> 2 = (2 / 2) \<up> 2 - - 8"

 then () else error "thm square_explicit1 CHANGED";

 val thm = @{thm root_plus_minus};

 val SOME (t,asm) = rewrite_ thy dummy_ord PolyEq_erls true thm t;

 if UnparseC.term t =

 "2 / 2 - x = sqrt ((2 / 2) \<up> 2 - - 8) \<or>\n2 / 2 - x = - 1 * sqrt ((2 / 2) \<up> 2 - - 8)"

 then () else error "thm root_plus_minus CHANGED";

 (*the thm bdv_explicit2* here required to be constrained to ::real*)

 val thm = @{thm bdv_explicit2};

 val SOME (t,asm) = rewrite_inst_ thy dummy_ord Rule_Set.Empty true inst thm t;

 if UnparseC.term t =

 "2 / 2 - x = sqrt ((2 / 2) \<up> 2 - - 8) \<or>\n- 1 * x = - (2 / 2) + - 1 * sqrt ((2 / 2) \<up> 2 - - 8)"

 then () else error "thm bdv_explicit2 CHANGED";

 val thm = @{thm bdv_explicit3};

 val SOME (t,asm) = rewrite_inst_ thy dummy_ord Rule_Set.Empty true inst thm t;

 if UnparseC.term t =

 "2 / 2 - x = sqrt ((2 / 2) \<up> 2 - - 8) \<or>\nx = - 1 * (- (2 / 2) + - 1 * sqrt ((2 / 2) \<up> 2 - - 8))"

 then () else error "thm bdv_explicit3 CHANGED";

 val thm = @{thm bdv_explicit2};

 val SOME (t,asm) = rewrite_inst_ thy dummy_ord Rule_Set.Empty true inst thm t;

 if UnparseC.term t =

 "- 1 * x = - (2 / 2) + sqrt ((2 / 2) \<up> 2 - - 8) \<or>\nx = - 1 * (- (2 / 2) + - 1 * sqrt ((2 / 2) \<up> 2 - - 8))"

 then () else error "thm bdv_explicit2 CHANGED";

 val rls = calculate_RootRat;