(* Title:  Knowledge/polyeq-1.sml

           testexamples for PolyEq, poynomial equations and equational systems

   Author: Richard Lang 2003  

   (c) due to copyright terms

WN030609: some expls dont work due to unfinished handling of 'expanded terms';

          others marked with TODO have to be checked, too.

*)

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

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

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

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

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

"----------- equality (2 +(-1)*x + x^^^2 = (0::real)) ----------------------------------------";

"----------- equality (-2 +(-1)*x + 1*x^^^2 = 0) ---------------------------------------------";

"----------- equality (-2 + x + x^^^2 = 0) ---------------------------------------------------";

"----------- equality (2 + x + x^^^2 = 0) ----------------------------------------------------";

"----------- equality (-2 + x + 1*x^^^2 = 0)) ------------------------------------------------";

"----------- equality (1*x +   x^^^2 = 0) ----------------------------------------------------";

"----------- equality (1*x + 1*x^^^2 = 0) ----------------------------------------------------";

"----------- equality (x +   x^^^2 = 0) ------------------------------------------------------";

"----------- equality (x + 1*x^^^2 = 0) ------------------------------------------------------";

"----------- equality (-4 + x^^^2 = 0) -------------------------------------------------------";

"----------- equality (4 + 1*x^^^2 = 0) -------------------------------------------------------";

"----------- equality (1 +(-1)*x + 2*x^^^2 = 0) ----------------------------------------------";

"----------- equality (-1 + x + 2*x^^^2 = 0) -------------------------------------------------";

"----------- equality (1 + x + 2*x^^^2 = 0) --------------------------------------------------";

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

"----------- (-8 - 2*x + x^^^2 = 0),  by rewriting ---------------";

"----------- (-16 + 4*x + 2*x^^^2 = 0), --------------------------";

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

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

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

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

"----------- (-147 + 3*x^^^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)^^^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 ---------------------";

(* Rewrite.trace_on:=true;

 Rewrite.trace_on:=false;

*)

 val t1 = (Thm.term_of o the o (parse thy)) "lhs (-8 - 2*x + x^^^2 = 0)";

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

 if ((UnparseC.term t) = "-8 - 2 * x + x ^^^ 2") then ()

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

 val t2 = (Thm.term_of o the o (parse thy)) "(-8 - 2*x + x^^^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 (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 (parse thy)) "(-8 + (-1)*2*x + x^^^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 (parse thy)) "(lhs (-8 + (-1)*2*x + x^^^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 (parse thy)) "(lhs (-8 - 2*x + x^^^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 (parse thy))"((-8 - 2*x + x^^^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 (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 (parse thy)) 

	      "((-8 - 2*x + x^^^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 (parse thy)) 

	      "((-8 - 2*x + x^^^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";

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

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

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

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

if match_pbl fmz (get_pbt ["expanded","univariate","equation"]) =

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

            With = [], 

            Given = [Correct "equality (-8 - 2 * x + x ^^^ 2 = 0)", Correct "solveFor x"], 

            Where = [Correct "matches (?a = 0) (-8 - 2 * x + x ^^^ 2 = 0)", 

                     Correct "lhs (-8 - 2 * x + x ^^^ 2 = 0) is_expanded_in x"], 

            Relate = []}

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

if match_pbl fmz (get_pbt ["degree_2","expanded","univariate","equation"]) =

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

            With = [], 

            Given = [Correct "equality (-8 - 2 * x + x ^^^ 2 = 0)", Correct "solveFor x"], 

            Where = [Correct "lhs (-8 - 2 * x + x ^^^ 2 = 0) has_degree_in x = 2"], 

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

then () else error "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 = (Thm.term_of o the o (parse thy)) "a*b - (a+b)*x + x^^^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 ^^^ 2)) = 0";

  val SOME (t,_) = 

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

  UnparseC.term t;

  "x ^^^ 2 + (-1 * (b * x) + (-1 * (x * a) + b * a)) = 0";

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

(*"x ^^^ 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 ^^^ 2 + -1 * b * x + -1 * x * a + b * a = 0";

(* "x ^^^ 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 ^^^ 2 + (-1 * (b * x) + a * (b + -1 * x)) = 0"; 

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

  "x ^^^ 2 + (-1 * (b * x)) + (b + -1 * x) * a = 0"*)

  (*das rewriting l"asst sich beobachten mit

Rewrite.trace_on := false;

  *)

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

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

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

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

Rewrite.trace_on := 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 (parse thy)) "1 + a * (x + b * x) + a^^^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 ^^^ 2";

 val t = (Thm.term_of o the o (parse thy)) "1 + a ^^^2 * x + b * a + 7*a^^^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 ^^^ 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 (parse thy)) "a ^^^2 * x + 7 * a^^^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 ^^^ 2";

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

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

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

"----------- 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 (parse thy)) "a")];

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

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

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

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

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

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

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

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

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

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

if ord_make_polynomial_in 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 (parse thy)) "-1 * a * x";

  val bb = (Thm.term_of o the o (parse thy)) "x^^^3";

  ord_make_polynomial_in true thy substx (aa, bb);

  true; (* => LESS *) 

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

  val bb = (Thm.term_of o the o (parse thy)) "x^^^3";

  ord_make_polynomial_in 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= (Thm.term_of o the o (parse thy)) "''bdv''";

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

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

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

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^^^3 + -1*x^^^2 + -1*x^^^3 + -14*x^^^2";

  val ppp  = (Thm.term_of o the o (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 ^^^ 2 + 0" then ()

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

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

if UnparseC.term t' = "-6 + -5 * x + -15 * x ^^^ 2 + 0" then ()

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

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

  val ttt = (Thm.term_of o the o (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";

(*============ inhibit exn WN120316 ==============================================

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

============ inhibit exn WN120316 ==============================================*)

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

"~~~~~ fun me, args:"; val (tac, (p:pos'), _, (pt:ctree)) = (nxt, p, [], pt);

"~~~~~ fun Step.by_tactic, args:"; val (tac, (ptp as (pt, p))) = (tac, (pt, p));

val Appl m = applicable_in p pt tac;

val Check_elementwise' (trm1, str, (trm2, trms)) = m;

UnparseC.term trm1 = "[z = 1 / 8 + sqrt (9 / 16) / 2, z = 1 / 8 + -1 * sqrt (9 / 16) / 2]";

str = "Assumptions";

UnparseC.term trm2 = "[z = 1 / 8 + sqrt (9 / 16) / 2, z = 1 / 8 + -1 * sqrt (9 / 16) / 2]";

UnparseC.terms trms = "[\"lhs (-1 / 8 + -1 * (1 / 8 + sqrt (9 / 16) / 2) / 4 +\n "^

  "    (1 / 8 + sqrt (9 / 16) / 2) ^^^ 2 =\n     0) is_poly_in 1 / 8 + sqrt (9 / 16) / 2\","^

  "\"lhs (-1 / 8 + -1 * (1 / 8 + sqrt (9 / 16) / 2) / 4 +\n     (1 / 8 + sqrt (9 / 16) / 2) ^^^ 2 =\n     0) "^

      "has_degree_in 1 / 8 + sqrt (9 / 16) / 2 =\n2\","^

  "\"lhs (-1 / 8 + -1 * (1 / 8 + -1 * sqrt (9 / 16) / 2) / 4 +\n     (1 / 8 + -1 * sqrt (9 / 16) / 2) ^^^ 2 =\n     0) is_poly_in 1 / 8 + -1 * sqrt (9 / 16) / 2\","^

  "\"lhs (-1 / 8 + -1 * (1 / 8 + -1 * sqrt (9 / 16) / 2) / 4 +\n     (1 / 8 + -1 * sqrt (9 / 16) / 2) ^^^ 2 =\n     0) has_degree_in 1 / 8 + -1 * sqrt (9 / 16) / 2 =\n2\"]";

(*TODO simplify assumptions (sqrt!) and check ERROR in has_degree_in*);

      (*if*) Tactic.for_specify' m; (*false*)

(*loc_solve_ (mI,m) ptp;

  WAS: not-found-in-program: NotLocatable from Term_Val1 (Const ("List...*)

"~~~~~ fun loc_solve_, args:"; val (m, (pt,pos)) = (m, ptp);

(*solve m (pt, pos);

  WAS: not-found-in-program: NotLocatable from Term_Val1 (Const ("List...*)

"~~~~~ fun Step_Solve.by_tactic , args:"; val (m, (pt, po as (p,p_))) = (m, (pt, pos));

Spec.e_metID = get_obj g_metID pt (par_pblobj pt p) (*false*);

        val thy' = get_obj g_domID pt (par_pblobj pt p);

	        val (is, sc) = resume_prog thy' (p,p_) pt;

		        val d = Rule_Set.empty;

(*locate_input_tactic (thy',srls) m  (pt,(p,p_)) (sc,d) is;

  WAS: not-found-in-program: NotLocatable from Term_Val1 (Const ("List...*)

"~~~~~ fun locate_input_tactic, args:"; val () = ();

(*----- outcommented during cleanup of args in lucas-interpreter.sml ------------------------\\* )

l = [] orelse ((last_elem o fst) p = 0 andalso snd p = Res) (*false*);

(*WAS val Reject_Tac1 _ =(go_scan_up1 (thy',srls,scr,d) ((E,l,a,v,S,b), [(m,EmptyMout,pt,p,[])]) )

  ... Accept_Tac1 ... is correct*)

"~~~~~ and go_scan_up1, args:"; val ((ys as (_,_,_,Prog sc,_)), ((E,l,a,v,S,b),ss)) =

   ((thy',ctxt,srls,scr,d), ((E,l,a,v,S,b), [(m,EmptyMout,pt,p,[])]));

1 < length l (*true*);

val up = drop_last l;

  UnparseC.term (at_location up sc);

  (at_location up sc);

(*WAS val Term_Val1 _ = scan_up1 ys ((E,up,a,v,S,b),ss) (at_location up sc)

      ... ???? ... is correct*)

"~~~~~ fun scan_up1, args:"; val ((ys as (y,ctxt,s,Prog sc,d)), (is as (E,l,a,v,S,b),ss), 

	   (Const ("HOL.Let",_) $ _)) = (ys, ((E,up,a,v,S,b),ss:step list), (at_location up sc));

      val l = drop_last l; (*comes from e, goes to Abs*)

      val (Const ("HOL.Let",_) $ e $ (Abs (i,T,body))) = at_location l sc;

      val i = mk_Free (i, T);

      val E = Env.update E (i, v);

(*Type error ...: Can't unify _a to pos * pos_ (Incompatible types)*)

val [(tac_, mout, ctree, pos', xxx)] = ss;

val ss = [(tac_, mout, ctree, pos', []:(pos * pos_) list)];

(*WAS val Reject_Tac1 iss = scan_dn1 (((y,s),d),ORundef) ((E, l@[R,D], a,v,S,b),ss) body

      ... Accept_Tac1 ... is correct*)

"~~~~~ fun scan_dn1, args:"; val ((((thy',sr),d),ap), (is as (E,l,a,v,S,b), (m,_,pt,(p,p_),c)::ss), t) =

     ((((y,s),d),ORundef), ((E, l@[R,D], a,v,S,b),ss), body);

val (Program.Tac stac, a') = check_leaf "locate" thy' sr (E, (a, v)) t

             val ctxt = get_ctxt pt (p,p_)

             val p' = lev_on p : pos;

(* WAS val Not_Associated = associate pt d (m, stac)

      ... Associated ... is correct*)

"~~~~~ fun associate, args:"; val (pt, _, (m as Check_elementwise' (consts,_,(consts_chkd,_))),

    (Const ("Prog_Tac.Check'_elementwise",_) $ consts' $ _)) = (pt, d, m, stac);

UnparseC.term consts;

UnparseC.term consts';

if consts = consts' (*WAS false*) then () else error "Check_elementwise changed";

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

( *----- outcommented during cleanup of args in lucas-interpreter.sml ------------------------//*)

"----------- equality (2 +(-1)*x + x^^^2 = (0::real)) ----------------------------------------";

"----------- equality (2 +(-1)*x + x^^^2 = (0::real)) ----------------------------------------";

"----------- equality (2 +(-1)*x + x^^^2 = (0::real)) ----------------------------------------";

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

val fmz = ["equality (2 +(-1)*x + x^^^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 ^^^ 2 = 0) is_poly_in x\"," ^

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

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

"----------- equality (-2 +(-1)*x + 1*x^^^2 = 0) ---------------------------------------------";

"----------- equality (-2 +(-1)*x + 1*x^^^2 = 0) ---------------------------------------------";

"----------- equality (-2 +(-1)*x + 1*x^^^2 = 0) ---------------------------------------------";

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

val fmz = ["equality (-2 +(-1)*x + 1*x^^^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 = e_pos'; 

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

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

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 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^^^2 = 0) ---------------------------------------------------";

"----------- equality (-2 + x + x^^^2 = 0) ---------------------------------------------------";

"----------- equality (-2 + x + x^^^2 = 0) ---------------------------------------------------";

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

(*EP-9*)

val fmz = ["equality (-2 + x + x^^^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 FormKF "[x = 1, x = -2]" => ()

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

"----------- equality (2 + x + x^^^2 = 0) ----------------------------------------------------";

"----------- equality (2 + x + x^^^2 = 0) ----------------------------------------------------";

"----------- equality (2 + x + x^^^2 = 0) ----------------------------------------------------";

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

val fmz = ["equality (2 + x + x^^^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^^^2 = 0";

"TODO 2 + x + x^^^2 = 0";

"TODO 2 + x + x^^^2 = 0";

"----------- equality (-2 + x + 1*x^^^2 = 0)) ------------------------------------------------";

"----------- equality (-2 + x + 1*x^^^2 = 0)) ------------------------------------------------";

"----------- equality (-2 + x + 1*x^^^2 = 0)) ------------------------------------------------";

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

val fmz = ["equality (-2 + x + 1*x^^^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 FormKF "[x = 1, x = -2]" => ()

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

"----------- equality (1*x +   x^^^2 = 0) ----------------------------------------------------";

"----------- equality (1*x +   x^^^2 = 0) ----------------------------------------------------";

"----------- equality (1*x +   x^^^2 = 0) ----------------------------------------------------";

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

val fmz = ["equality (1*x +   x^^^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 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^^^2 = 0) ----------------------------------------------------";

"----------- equality (1*x + 1*x^^^2 = 0) ----------------------------------------------------";

"----------- equality (1*x + 1*x^^^2 = 0) ----------------------------------------------------";

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

val fmz = ["equality (1*x + 1*x^^^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 FormKF "[x = 0, x = -1]" => ()

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

"----------- equality (x +   x^^^2 = 0) ------------------------------------------------------";

"----------- equality (x +   x^^^2 = 0) ------------------------------------------------------";

"----------- equality (x +   x^^^2 = 0) ------------------------------------------------------";

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

(*EP-10*)

val fmz = ["equality (  x +   x^^^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 FormKF "[x = 0, x = -1]" => ()

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

"----------- equality (x + 1*x^^^2 = 0) ------------------------------------------------------";

"----------- equality (x + 1*x^^^2 = 0) ------------------------------------------------------";

"----------- equality (x + 1*x^^^2 = 0) ------------------------------------------------------";

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

val fmz = ["equality (x + 1*x^^^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 FormKF "[x = 0, x = -1]" => ()

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

"----------- equality (-4 + x^^^2 = 0) -------------------------------------------------------";

"----------- equality (-4 + x^^^2 = 0) -------------------------------------------------------";

"----------- equality (-4 + x^^^2 = 0) -------------------------------------------------------";

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

val fmz = ["equality (-4 + x^^^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 FormKF "[x = 2, x = -2]" => ()

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

"----------- equality (4 + 1*x^^^2 = 0) -------------------------------------------------------";

"----------- equality (4 + 1*x^^^2 = 0) -------------------------------------------------------";

"----------- equality (4 + 1*x^^^2 = 0) -------------------------------------------------------";

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

val fmz = ["equality (4 + 1*x^^^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^^^2 = 0";

"TODO 4 + 1*x^^^2 = 0";

"TODO 4 + 1*x^^^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^^^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 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^^^2 = 0) ----------------------------------------------";

"----------- equality (1 +(-1)*x + 2*x^^^2 = 0) ----------------------------------------------";

"----------- equality (1 +(-1)*x + 2*x^^^2 = 0) ----------------------------------------------";

val fmz = ["equality (1 +(-1)*x + 2*x^^^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^^^2 = 0";

"TODO 1 +(-1)*x + 2*x^^^2 = 0";

"TODO 1 +(-1)*x + 2*x^^^2 = 0";

"----------- equality (-1 + x + 2*x^^^2 = 0) -------------------------------------------------";

"----------- equality (-1 + x + 2*x^^^2 = 0) -------------------------------------------------";

"----------- equality (-1 + x + 2*x^^^2 = 0) -------------------------------------------------";

(*EP-11*)

val fmz = ["equality (-1 + x + 2*x^^^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 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^^^2 = 0) --------------------------------------------------";

"----------- equality (1 + x + 2*x^^^2 = 0) --------------------------------------------------";

"----------- equality (1 + x + 2*x^^^2 = 0) --------------------------------------------------";

val fmz = ["equality (1 + x + 2*x^^^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^^^2 = 0";

"TODO 1 + x + 2*x^^^2 = 0";

"TODO 1 + x + 2*x^^^2 = 0";

val fmz = ["equality (-2 + 1*x + x^^^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 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^^^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^^^2 = 0";

"TODO 2 + 1*x + x^^^2 = 0";

"TODO 2 + 1*x + x^^^2 = 0";

(*EP-12*)

val fmz = ["equality (-2 + x + x^^^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 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^^^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^^^2 = 0";

"TODO 2 + x + x^^^2 = 0";

"TODO 2 + x + x^^^2 = 0";

(*EP-13*)

val fmz = ["equality (-8 + 2*x^^^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 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^^^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^^^2 = 0";

"TODO 8+ 2*x^^^2 = 0";

"TODO 8+ 2*x^^^2 = 0";

(*EP-14*)

val fmz = ["equality (-4 + x^^^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 FormKF "[x = 2, x = -2]" => ()

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

val fmz = ["equality ( 4+ x^^^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^^^2 = 0";

"TODO 4+ x^^^2 = 0";

"TODO 4+ x^^^2 = 0";

(*EP-15*)

val fmz = ["equality (2*x + 2*x^^^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 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^^^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 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^^^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 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^^^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 FormKF "[x = 0, x = -1]" => ()

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

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

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

"----------- (-8 - 2*x + x^^^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^^^2 = 0),  by rewriting --- below

*)

 val fmz = ["equality (-8 - 2*x + x^^^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 ^^^ 2 = 0", nxt = Rewrite_Set_Inst ... "complete_square*)

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

(*"-8 + (2 / 2 - x) ^^^ 2 = (2 / 2) ^^^ 2", nxt = Rewrite("square_explicit1"*)

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

(*"(2 / 2 - x) ^^^ 2 = (2 / 2) ^^^ 2 - -8" nxt = Rewrite("root_plus_minus*)

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

(*"2 / 2 - x = sqrt ((2 / 2) ^^^ 2 - -8) |

   2 / 2 - x = - sqrt ((2 / 2) ^^^ 2 - -8)" nxt = Rewr_Inst("bdv_explicit2"*)

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

(*"2 / 2 - x = sqrt ((2 / 2) ^^^ 2 - -8) |

   -1*x = - (2 / 2) + - sqrt ((2 / 2) ^^^ 2 - -8)"nxt = R_Inst("bdv_explt2"*)

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

(*"-1 * x = - (2 / 2) + sqrt ((2 / 2) ^^^ 2 - -8) |

   -1 * x = (- (2 / 2) + - sqrt ((2 / 2) ^^^ 2 - -8))"nxt = bdv_explicit3*)

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

(*"-1 * x = - (2 / 2) + sqrt ((2 / 2) ^^^ 2 - -8) |

  x = -1 * (- (2 / 2) + - sqrt ((2 / 2) ^^^ 2 - -8))" nxt = bdv_explicit3*)

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

(*"x = -1 * (- (2 / 2) + sqrt ((2 / 2) ^^^ 2 - -8)) |

   x = -1 * (- (2 / 2) + - sqrt ((2 / 2) ^^^ 2 - -8))"nxt = calculate_Rational

   NOT IMPLEMENTED SINCE 2002 ------------------------------^^^^^^^^^^^^^^^^^^*)

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' (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 ^^^ 2 / 2 ^^^ 2 - -8),\n x = -1 * -1 + -1 * (-1 * sqrt (2 ^^^ 2 / 2 ^^^ 2 - -8))]"

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

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

"----------- (-8 - 2*x + x^^^2 = 0),  by rewriting ---------------";

"----------- (-8 - 2*x + x^^^2 = 0),  by rewriting ---------------";

"----------- (-8 - 2*x + x^^^2 = 0),  by rewriting ---------------";

(*stopped du 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^^^2 = (0::real)";

val rls = complete_square;

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

UnparseC.term t = "-8 + (2 / 2 - x) ^^^ 2 = (2 / 2) ^^^ 2";

val thm = ThmC.numerals_to_Free @{thm square_explicit1};

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

UnparseC.term t = "(2 / 2 - x) ^^^ 2 = (2 / 2) ^^^ 2 - -8";

val thm = ThmC.numerals_to_Free @{thm root_plus_minus};

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

UnparseC.term t = "2 / 2 - x = sqrt ((2 / 2) ^^^ 2 - -8) |"^

           "\n2 / 2 - x = -1 * sqrt ((2 / 2) ^^^ 2 - -8)";

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

val thm = ThmC.numerals_to_Free @{thm bdv_explicit2};

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

UnparseC.term t = "2 / 2 - x = sqrt ((2 / 2) ^^^ 2 - -8) |"^

              "\n-1 * x = - (2 / 2) + -1 * sqrt ((2 / 2) ^^^ 2 - -8)";

val thm = ThmC.numerals_to_Free @{thm bdv_explicit3};

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

UnparseC.term t = "2 / 2 - x = sqrt ((2 / 2) ^^^ 2 - -8) |"^

                   "\nx = -1 * (- (2 / 2) + -1 * sqrt ((2 / 2) ^^^ 2 - -8))";

val thm = ThmC.numerals_to_Free @{thm bdv_explicit2};

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

UnparseC.term t = "-1 * x = - (2 / 2) + sqrt ((2 / 2) ^^^ 2 - -8) |"^

                "\nx = -1 * (- (2 / 2) + -1 * sqrt ((2 / 2) ^^^ 2 - -8))";

val rls = calculate_RootRat;

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