(* 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 ---------------------";

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

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

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

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

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

val thy = @{theory};

val ctxt = Proof_Context.init_global thy;

 val t1 = TermC.parseNEW' ctxt "lhs (-8 - 2*x + x \<up> 2 = 0)";

 val SOME (t,_) = rewrite_set_ ctxt false PolyEq_prls t1;

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

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

 val t2 = TermC.parseNEW' ctxt "(-8 - 2*x + x \<up> 2) is_expanded_in x";

 val SOME (t,_) = rewrite_set_ ctxt false PolyEq_prls t2;

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

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

 val t0 = TermC.parseNEW' ctxt "(sqrt(x)) is_poly_in x";

 val SOME (t,_) = rewrite_set_ ctxt false PolyEq_prls t0;

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

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

 val t3 = TermC.parseNEW' ctxt "(-8 + (- 1)*2*x + x \<up> 2) is_poly_in x";

 val SOME (t,_) = rewrite_set_ ctxt false PolyEq_prls t3;

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

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

 val t4 = TermC.parseNEW' ctxt "(lhs (-8 + (- 1)*2*x + x \<up> 2 = 0)) is_expanded_in x";

 val SOME (t,_) = rewrite_set_ ctxt false PolyEq_prls t4;

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

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

 val t6 = TermC.parseNEW' ctxt "(lhs (-8 - 2*x + x \<up> 2 = 0)) is_expanded_in x";

 val SOME (t,_) = rewrite_set_ ctxt false PolyEq_prls t6;

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

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

 val t3 = TermC.parseNEW' ctxt"((-8 - 2*x + x \<up> 2) has_degree_in x) = 2";

 val SOME (t,_) = rewrite_set_ ctxt false PolyEq_prls t3;

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

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

 val t3 = TermC.parseNEW' ctxt "((sqrt(x)) has_degree_in x) = 2";

 val SOME (t,_) = rewrite_set_ ctxt false PolyEq_prls t3;

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

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

 val t4 = TermC.parseNEW' ctxt 

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

 val SOME (t,_) = rewrite_set_ ctxt false PolyEq_prls t4;

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

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

val t5 = TermC.parseNEW' ctxt 

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

 val SOME (t,_) = rewrite_set_ ctxt false PolyEq_prls t5;

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

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

"----------- 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]";

"----------- 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 = TermC.parseNEW' ctxt "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 = TermC.parseNEW' ctxt "1 + a * x + b * x";

  val bdv = TermC.parseNEW' ctxt "bdv";

  val a = TermC.parseNEW' ctxt "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 = TermC.parseNEW' ctxt "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 = TermC.parseNEW' ctxt "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 = TermC.parseNEW' ctxt "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";

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

"----------- 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";

"----------- 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, TermC.parseNEW' ctxt "a::real")];

  val substb = [(TermC.empty, TermC.parseNEW' ctxt "b::real")];

  val substx = [(TermC.empty, TermC.parseNEW' ctxt "x::real")];

  val x1 = TermC.parseNEW' ctxt "a + b + x::real";

  val x2 = TermC.parseNEW' ctxt "a + x + b::real";

  val x3 = TermC.parseNEW' ctxt "a + x + b::real";

  val x4 = TermC.parseNEW' ctxt "x + a + b::real";

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 = TermC.parseNEW' ctxt "- 1 * a * x::real";

  val bb = TermC.parseNEW' ctxt "x \<up> 3::real";

if ord_make_polynomial_in false(*true*) thy substx (aa, bb) = true(*LESS *) then ()

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

  val aa = TermC.parseNEW' ctxt "- 1 * a * x";

  val bb = TermC.parseNEW' ctxt "x \<up> 3";

if ord_make_polynomial_in false(*true*) thy substa (aa, bb) = false(*GREATER*) then ()

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

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

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

  val bdv= TermC.parseNEW' ctxt "bdv ::real";

  val x  = TermC.parseNEW' ctxt "x ::real";

  val a  = TermC.parseNEW' ctxt "a ::real";

  val b  = TermC.parseNEW' ctxt "b ::real";

val SOME (t',_) = rewrite_set_inst_ ctxt 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_ ctxt false [(bdv,b)] make_polynomial_in x2;

val SOME (t',_) = rewrite_set_inst_ ctxt 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  = TermC.parseNEW' ctxt ppp';

val SOME (t', _) = rewrite_set_inst_ ctxt 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 = TermC.parseNEW' ctxt ttt';

val SOME (uuu,_) = rewrite_set_inst_ ctxt 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_ ctxt false make_polynomial ttt;

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

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

"----------- 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 ============================================*)

"----------- 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";

"----------- 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";

"----------- 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]";

"----------- 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]";

"----------- 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";

"----------- 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]";

"----------- 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]";

"----------- 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]";

"----------- 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)", "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]";

"----------- 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]";

"----------- 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]";

"----------- 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";

"-------------------- 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]";

"----------- 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";

"----------- 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]";

"----------- 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]";

"----------- (-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*)