Mercurial Mercurial > wneuper > isa / comparison
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
test/Tools/isac/Knowledge/polyeq.sml
branchdecompose-isar
changeset 42272 dcc5d2601cf7
parent 42260 537d95d1fdb2
child 42283 b95f0dde56c1
equal deleted inserted replaced
42269:b8a255b0ba3b 42272:dcc5d2601cf7 
    23 "----------- interSteps ([1],Res); on Schalk Is86Bsp5-------------";
 
    23 "----------- interSteps ([1],Res); on Schalk Is86Bsp5-------------";
 
    24 "-----------------------------------------------------------------";
 
    24 "-----------------------------------------------------------------";
 
    25 "-----------------------------------------------------------------";
 
    25 "-----------------------------------------------------------------";
 
    26 "-----------------------------------------------------------------";
 
    26 "-----------------------------------------------------------------";
 
    27 
    27 
    28 val c = []; print_depth 5;
 
       
    29 
       
    30 "----------- tests on predicates in problems ---------------------";
 
    28 "----------- tests on predicates in problems ---------------------";
 
    31 "----------- tests on predicates in problems ---------------------";
 
    29 "----------- tests on predicates in problems ---------------------";
 
    32 "----------- tests on predicates in problems ---------------------";
 
    30 "----------- tests on predicates in problems ---------------------";
 
    33 (* 
    31 (* 
    34  trace_rewrite:=true;
 
    32  trace_rewrite:=true;
 
   110 
   108 
   111 "----------- lin.eq degree_0 -------------------------------------";
 
   109 "----------- lin.eq degree_0 -------------------------------------";
 
   112 "----------- lin.eq degree_0 -------------------------------------";
 
   110 "----------- lin.eq degree_0 -------------------------------------";
 
   113 "----------- lin.eq degree_0 -------------------------------------";
 
   111 "----------- lin.eq degree_0 -------------------------------------";
 
   114 "----- d0_false ------";
 
   112 "----- d0_false ------";
 
   115 (*=== inhibit exn WN110906 ======================================================
 
   113 (*=== inhibit exn WN110914: declare_constraints doesnt work with num_str ========
 
   116 val fmz = ["equality (1 = (0::real))", "solveFor x", "solutions L"];
 
   114 val fmz = ["equality (1 = (0::real))", "solveFor x", "solutions L"];
 
   117 val (dI',pI',mI') = ("PolyEq",["degree_0","polynomial","univariate","equation"],
 
   115 val (dI',pI',mI') = ("PolyEq",["degree_0","polynomial","univariate","equation"],
 
   118                      ["PolyEq","solve_d0_polyeq_equation"]);
 
   116                      ["PolyEq","solve_d0_polyeq_equation"]);
 
   119 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
 
   117 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
 
   120 val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   118 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
   121 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   119 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
   122 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   120 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
   123 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   121 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
   124 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   122 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
   125 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   123 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
   126 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[]")) => ()
 
   124 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[]")) => ()
 
   127 	 | _ => error "polyeq.sml: diff.behav. in 1 = 0 -> []";
 
   125 	 | _ => error "polyeq.sml: diff.behav. in 1 = 0 -> []";
 
   128 
   126 
   129 "----- d0_true ------";
 
   127 "----- d0_true ------";
 
   130 (*EP-7*)
 
       
   131 val fmz = ["equality (0 = (0::real))", "solveFor x","solutions L"];
 
   128 val fmz = ["equality (0 = (0::real))", "solveFor x","solutions L"];
 
   132 val (dI',pI',mI') = ("PolyEq",["degree_0","polynomial","univariate","equation"],
 
   129 val (dI',pI',mI') = ("PolyEq",["degree_0","polynomial","univariate","equation"],
 
   133                      ["PolyEq","solve_d0_polyeq_equation"]);
 
   130                      ["PolyEq","solve_d0_polyeq_equation"]);
 
   134 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
 
   131 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
 
   135 val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   132 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
   136 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   133 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
   137 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   134 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
   138 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   135 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
   139 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   136 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
   140 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   137 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
   141 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"UniversalList")) => ()
 
   138 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"UniversalList")) => ()
 
   142 	 | _ => error "polyeq.sml: diff.behav. in 0 = 0 -> UniversalList";
 
   139 	 | _ => error "polyeq.sml: diff.behav. in 0 = 0 -> UniversalList";
 
   143 ============ inhibit exn WN110906 ============================================*)
 
   140 ============ inhibit exn WN110914 ============================================*)
 
   144 
   141 
   145 "----------- test thm's d2_pq_formulsxx[_neg]---------------------";
 
   142 "----------- test thm's d2_pq_formulsxx[_neg]---------------------";
 
   146 "----------- test thm's d2_pq_formulsxx[_neg]---------------------";
 
   143 "----------- test thm's d2_pq_formulsxx[_neg]---------------------";
 
   147 "----------- test thm's d2_pq_formulsxx[_neg]---------------------";
 
   144 "----------- test thm's d2_pq_formulsxx[_neg]---------------------";
 
   148 "----- d2_pqformula1 ------!!!!";
 
   145 "----- d2_pqformula1 ------!!!!";
 
   228     (Const ("Script.Check'_elementwise",_) $ consts' $ _)) = (pt, d, m, stac);
 
   225     (Const ("Script.Check'_elementwise",_) $ consts' $ _)) = (pt, d, m, stac);
 
   229 term2str consts;
 
   226 term2str consts;
 
   230 term2str consts';
 
   227 term2str consts';
 
   231 if consts = consts' (*WAS false*) then () else error "Check_elementwise changed";
 
   228 if consts = consts' (*WAS false*) then () else error "Check_elementwise changed";
 
   232 (*[z = 1 / 8 + sqrt (9 / 16) / 2, z = 1 / 8 + -1 * sqrt (9 / 16) / 2] TODO sqrt*)
 
   229 (*[z = 1 / 8 + sqrt (9 / 16) / 2, z = 1 / 8 + -1 * sqrt (9 / 16) / 2] TODO sqrt*)
 
       
   230 *}
 
       
   231 
       
   232 
       
   233 ML {*
 
   233 
   234 
   234 "----- d2_pqformula1_neg ------";
 
   235 "----- d2_pqformula1_neg ------";
 
   235 (*EP-8*)
 
   236 val fmz = ["equality (2 +(-1)*x + x^^^2 = (0::real))", "solveFor x","solutions L"];
 
   236 val fmz = ["equality ( 2 +(-1)*x + x^^^2 = 0)", "solveFor x","solutions L"];
 
       
   237 val (dI',pI',mI') = ("PolyEq",["pqFormula","degree_2","polynomial","univariate","equation"], ["PolyEq","solve_d2_polyeq_pq_equation"]);
 
   237 val (dI',pI',mI') = ("PolyEq",["pqFormula","degree_2","polynomial","univariate","equation"], ["PolyEq","solve_d2_polyeq_pq_equation"]);
 
   238 (*val p = e_pos'; val c = []; 
   238 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
 
   239 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
 
   239 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
   240 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
 
   240 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
   241 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
 
   241 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
   242 val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   242 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
   243 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   243 *}
 
   244 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   244 ML {*
 
   245 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   245 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
   246 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
       
   247 (*### or2list False
 
   246 (*### or2list False
 
   248   ([1],Res)  False   Or_to_List)*)
 
   247   ([1],Res)  False   Or_to_List)*)
 
   249 val (p,_,f,nxt,_,pt) = me nxt p c pt; 
   248 val (p,_,f,nxt,_,pt) = me nxt p [] pt; 
   250 (*### or2list False
 
   249 (*### or2list False
 
   251   ([2],Res)  []      Check_elementwise "Assumptions"*)
 
   250   ([2],Res)  []      Check_elementwise "Assumptions"*)
 
   252 val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   251 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
   253 val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   252 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
   254 val asm = get_assumptions_ pt p;
 
   253 val asm = get_assumptions_ pt p;
 
   255 if f = Form' (FormKF (~1,EdUndef,0,Nundef,"[]")) andalso asm = [] then ()
 
   254 if f = Form' (FormKF (~1,EdUndef,0,Nundef,"[]")) andalso asm = [] then ()
 
   256 else error "polyeq.sml: diff.behav. in 2 +(-1)*x + x^^^2 = 0";
 
   255 else error "polyeq.sml: diff.behav. in 2 +(-1)*x + x^^^2 = 0";
 
       
   256 *}
 
       
   257 ML {*
 
   257 
   258 
   258 "----- d2_pqformula2 ------";
 
   259 "----- d2_pqformula2 ------";
 
   259 val fmz = ["equality (-2 +(-1)*x + 1*x^^^2 = 0)", "solveFor x","solutions L"];
 
   260 val fmz = ["equality (-2 +(-1)*x + 1*x^^^2 = 0)", "solveFor x","solutions L"];
 
   260 val (dI',pI',mI') = ("PolyEq",["pqFormula","degree_2","polynomial","univariate","equation"],
 
   261 val (dI',pI',mI') = ("PolyEq",["pqFormula","degree_2","polynomial","univariate","equation"],
 
   261                      ["PolyEq","solve_d2_polyeq_pq_equation"]);
 
   262                      ["PolyEq","solve_d2_polyeq_pq_equation"]);
 
   262 (*val p = e_pos'; val c = []; 
   263 (*val p = e_pos'; 
   263 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
 
   264 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
 
   264 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
 
   265 val (p,_,f,nxt,_,pt) = me (mI,m) p [] EmptyPtree;*)
 
   265 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
 
   266 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
 
   266 val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   267 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
   267 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   268 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
   268 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   269 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
   269 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   270 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
   270 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   271 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
   271 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   272 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
   272 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   273 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
   273 val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   274 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
   274 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 2, x = -1]")) => ()
 
   275 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 2, x = -1]")) => ()
 
   275 	 | _ => error "polyeq.sml: diff.behav. in -2 + (-1)*x + x^2 = 0 -> [x = 2, x = -1]";
 
   276 	 | _ => error "polyeq.sml: diff.behav. in -2 + (-1)*x + x^2 = 0 -> [x = 2, x = -1]";
 
   276 
   277 
   277 
   278 
   278 "----- d2_pqformula2_neg ------";
 
   279 "----- d2_pqformula2_neg ------";
 
   281                      ["PolyEq","solve_d2_polyeq_pq_equation"]);
 
   282                      ["PolyEq","solve_d2_polyeq_pq_equation"]);
 
   282 (*val p = e_pos'; val c = []; 
   283 (*val p = e_pos'; val c = []; 
   283 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
 
   284 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
 
   284 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
 
   285 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
 
   285 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
 
   286 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
 
   286 val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   287 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
   287 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   288 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
   288 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   289 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
   289 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   290 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
   290 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   291 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
   291 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   292 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
   292 val (p,_,f,nxt,_,pt) = me nxt p c pt; 
   293 val (p,_,f,nxt,_,pt) = me nxt p [] pt; 
   293 "TODO 2 +(-1)*x + 1*x^^^2 = 0";
 
   294 "TODO 2 +(-1)*x + 1*x^^^2 = 0";
 
   294 "TODO 2 +(-1)*x + 1*x^^^2 = 0";
 
   295 "TODO 2 +(-1)*x + 1*x^^^2 = 0";
 
   295 "TODO 2 +(-1)*x + 1*x^^^2 = 0";
 
   296 "TODO 2 +(-1)*x + 1*x^^^2 = 0";
 
   296 
   297 
   297 
   298 
   302                      ["PolyEq","solve_d2_polyeq_pq_equation"]);
 
   303                      ["PolyEq","solve_d2_polyeq_pq_equation"]);
 
   303 (*val p = e_pos'; val c = []; 
   304 (*val p = e_pos'; val c = []; 
   304 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
 
   305 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
 
   305 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
 
   306 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
 
   306 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
 
   307 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
 
   307 val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   308 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
   308 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   309 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
   309 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   310 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
   310 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   311 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
   311 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   312 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
   312 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   313 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
   313 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   314 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
   314 val (p,_,f,nxt,_,pt) = me nxt p c pt; 
   315 val (p,_,f,nxt,_,pt) = me nxt p [] pt; 
   315 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 1, x = -2]")) => ()
 
   316 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 1, x = -2]")) => ()
 
   316 	 | _ => error "polyeq.sml: diff.behav. in  -2 + x + x^2 = 0-> [x = 1, x = -2]";
 
   317 	 | _ => error "polyeq.sml: diff.behav. in  -2 + x + x^2 = 0-> [x = 1, x = -2]";
 
   317 
   318 
   318 "----- d2_pqformula3_neg ------";
 
   319 "----- d2_pqformula3_neg ------";
 
   319 val fmz = ["equality ( 2 + x + x^^^2 = 0)", "solveFor x","solutions L"];
 
   320 val fmz = ["equality ( 2 + x + x^^^2 = 0)", "solveFor x","solutions L"];
 
   321                      ["PolyEq","solve_d2_polyeq_pq_equation"]);
 
   322                      ["PolyEq","solve_d2_polyeq_pq_equation"]);
 
   322 (*val p = e_pos'; val c = []; 
   323 (*val p = e_pos'; val c = []; 
   323 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
 
   324 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
 
   324 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
 
   325 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
 
   325 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
 
   326 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
 
   326 val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   327 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
   327 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   328 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
   328 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   329 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
   329 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   330 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
   330 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   331 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
   331 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   332 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
   332 val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   333 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
   333 "TODO 2 + x + x^^^2 = 0";
 
   334 "TODO 2 + x + x^^^2 = 0";
 
   334 "TODO 2 + x + x^^^2 = 0";
 
   335 "TODO 2 + x + x^^^2 = 0";
 
   335 "TODO 2 + x + x^^^2 = 0";
 
   336 "TODO 2 + x + x^^^2 = 0";
 
   336 
   337 
   337 
   338 
   341                      ["PolyEq","solve_d2_polyeq_pq_equation"]);
 
   342                      ["PolyEq","solve_d2_polyeq_pq_equation"]);
 
   342 (*val p = e_pos'; val c = []; 
   343 (*val p = e_pos'; val c = []; 
   343 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
 
   344 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
 
   344 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
 
   345 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
 
   345 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
 
   346 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
 
   346 val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   347 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
   347 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   348 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
   348 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   349 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
   349 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   350 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
   350 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   351 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
   351 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   352 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
   352 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   353 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
   353 val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   354 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
   354 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 1, x = -2]")) => ()
 
   355 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 1, x = -2]")) => ()
 
   355 	 | _ => error "polyeq.sml: diff.behav. in  -2 + x + 1*x^^^2 = 0 -> [x = 1, x = -2]";
 
   356 	 | _ => error "polyeq.sml: diff.behav. in  -2 + x + 1*x^^^2 = 0 -> [x = 1, x = -2]";
 
   356 
   357 
   357 "----- d2_pqformula4_neg ------";
 
   358 "----- d2_pqformula4_neg ------";
 
   358 val fmz = ["equality ( 2 + x + 1*x^^^2 = 0)", "solveFor x","solutions L"];
 
   359 val fmz = ["equality ( 2 + x + 1*x^^^2 = 0)", "solveFor x","solutions L"];
 
   360                      ["PolyEq","solve_d2_polyeq_pq_equation"]);
 
   361                      ["PolyEq","solve_d2_polyeq_pq_equation"]);
 
   361 (*val p = e_pos'; val c = []; 
   362 (*val p = e_pos'; val c = []; 
   362 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
 
   363 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
 
   363 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
 
   364 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
 
   364 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
 
   365 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
 
   365 val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   366 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
   366 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   367 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
   367 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   368 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
   368 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   369 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
   369 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   370 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
   370 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   371 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
   371 "TODO 2 + x + 1*x^^^2 = 0";
 
   372 "TODO 2 + x + 1*x^^^2 = 0";
 
   372 "TODO 2 + x + 1*x^^^2 = 0";
 
   373 "TODO 2 + x + 1*x^^^2 = 0";
 
   373 "TODO 2 + x + 1*x^^^2 = 0";
 
   374 "TODO 2 + x + 1*x^^^2 = 0";
 
   374 
   375 
   375 "----- d2_pqformula5 ------";
 
   376 "----- d2_pqformula5 ------";
 
   378                      ["PolyEq","solve_d2_polyeq_pq_equation"]);
 
   379                      ["PolyEq","solve_d2_polyeq_pq_equation"]);
 
   379 (*val p = e_pos'; val c = []; 
   380 (*val p = e_pos'; val c = []; 
   380 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
 
   381 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
 
   381 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
 
   382 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
 
   382 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
 
   383 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
 
   383 val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   384 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
   384 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   385 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
   385 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   386 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
   386 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   387 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
   387 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   388 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
   388 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   389 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
   389 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   390 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
   390 val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   391 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
   391 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 0, x = -1]")) => ()
 
   392 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 0, x = -1]")) => ()
 
   392 	 | _ => error "polyeq.sml: diff.behav. in  1*x +   x^2 = 0 -> [x = 0, x = -1]";
 
   393 	 | _ => error "polyeq.sml: diff.behav. in  1*x +   x^2 = 0 -> [x = 0, x = -1]";
 
   393 
   394 
   394 "----- d2_pqformula6 ------";
 
   395 "----- d2_pqformula6 ------";
 
   395 val fmz = ["equality (1*x + 1*x^^^2 = 0)", "solveFor x","solutions L"];
 
   396 val fmz = ["equality (1*x + 1*x^^^2 = 0)", "solveFor x","solutions L"];
 
   397                      ["PolyEq","solve_d2_polyeq_pq_equation"]);
 
   398                      ["PolyEq","solve_d2_polyeq_pq_equation"]);
 
   398 (*val p = e_pos'; val c = []; 
   399 (*val p = e_pos'; val c = []; 
   399 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
 
   400 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
 
   400 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
 
   401 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
 
   401 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
 
   402 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
 
   402 val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   403 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
   403 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   404 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
   404 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   405 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
   405 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   406 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
   406 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   407 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
   407 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   408 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
   408 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   409 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
   409 val (p,_,f,nxt,_,pt) = me nxt p c pt; 
   410 val (p,_,f,nxt,_,pt) = me nxt p [] pt; 
   410 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 0, x = -1]")) => ()
 
   411 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 0, x = -1]")) => ()
 
   411 	 | _ => error "polyeq.sml: diff.behav. in  1*x + 1*x^2 = 0 -> [x = 0, x = -1]";
 
   412 	 | _ => error "polyeq.sml: diff.behav. in  1*x + 1*x^2 = 0 -> [x = 0, x = -1]";
 
   412 
   413 
   413 "----- d2_pqformula7 ------";
 
   414 "----- d2_pqformula7 ------";
 
   414 (*EP-10*)
 
   415 (*EP-10*)
 
   417                      ["PolyEq","solve_d2_polyeq_pq_equation"]);
 
   418                      ["PolyEq","solve_d2_polyeq_pq_equation"]);
 
   418 (*val p = e_pos'; val c = []; 
   419 (*val p = e_pos'; val c = []; 
   419 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
 
   420 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
 
   420 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
 
   421 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
 
   421 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
 
   422 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
 
   422 val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   423 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
   423 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   424 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
   424 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   425 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
   425 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   426 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
   426 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   427 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
   427 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   428 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
   428 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   429 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
   429 val (p,_,f,nxt,_,pt) = me nxt p c pt; 
   430 val (p,_,f,nxt,_,pt) = me nxt p [] pt; 
   430 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 0, x = -1]")) => ()
 
   431 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 0, x = -1]")) => ()
 
   431 	 | _ => error "polyeq.sml: diff.behav. in  x + x^2 = 0 -> [x = 0, x = -1]";
 
   432 	 | _ => error "polyeq.sml: diff.behav. in  x + x^2 = 0 -> [x = 0, x = -1]";
 
   432 
   433 
   433 "----- d2_pqformula8 ------";
 
   434 "----- d2_pqformula8 ------";
 
   434 val fmz = ["equality (  x + 1*x^^^2 = 0)", "solveFor x","solutions L"];
 
   435 val fmz = ["equality (  x + 1*x^^^2 = 0)", "solveFor x","solutions L"];
 
   437 (*val p = e_pos'; val c = []; 
   438 (*val p = e_pos'; val c = []; 
   438 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
 
   439 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
 
   439 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
 
   440 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
 
   440 
   441 
   441 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
 
   442 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
 
   442 val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   443 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
   443 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   444 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
   444 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   445 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
   445 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   446 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
   446 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   447 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
   447 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   448 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
   448 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   449 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
   449 val (p,_,f,nxt,_,pt) = me nxt p c pt; 
   450 val (p,_,f,nxt,_,pt) = me nxt p [] pt; 
   450 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 0, x = -1]")) => ()
 
   451 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 0, x = -1]")) => ()
 
   451 	 | _ => error "polyeq.sml: diff.behav. in  x + 1*x^2 = 0 -> [x = 0, x = -1]";
 
   452 	 | _ => error "polyeq.sml: diff.behav. in  x + 1*x^2 = 0 -> [x = 0, x = -1]";
 
   452 
   453 
   453 "----- d2_pqformula9 ------";
 
   454 "----- d2_pqformula9 ------";
 
   454 val fmz = ["equality (-4 + x^^^2 = 0)", "solveFor x","solutions L"];
 
   455 val fmz = ["equality (-4 + x^^^2 = 0)", "solveFor x","solutions L"];
 
   457 (*val p = e_pos'; val c = []; 
   458 (*val p = e_pos'; val c = []; 
   458 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
 
   459 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
 
   459 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
 
   460 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
 
   460 
   461 
   461 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
 
   462 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
 
   462 val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   463 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
   463 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   464 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
   464 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   465 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
   465 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   466 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
   466 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   467 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
   467 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   468 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
   468 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   469 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
   469 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 2, x = -2]")) => ()
 
   470 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 2, x = -2]")) => ()
 
   470 	 | _ => error "polyeq.sml: diff.behav. in -4 + x^2 = 0 -> [x = 2, x = -2]";
 
   471 	 | _ => error "polyeq.sml: diff.behav. in -4 + x^2 = 0 -> [x = 2, x = -2]";
 
   471 
   472 
   472 
   473 
   473 "----- d2_pqformula10_neg ------";
 
   474 "----- d2_pqformula10_neg ------";
 
   477 (*val p = e_pos'; val c = []; 
   478 (*val p = e_pos'; val c = []; 
   478 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
 
   479 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
 
   479 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
 
   480 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
 
   480 
   481 
   481 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
 
   482 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
 
   482 val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   483 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
   483 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   484 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
   484 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   485 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
   485 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   486 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
   486 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   487 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
   487 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   488 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
   488 val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   489 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
   489 "TODO 4 + x^^^2 = 0";
 
   490 "TODO 4 + x^^^2 = 0";
 
   490 "TODO 4 + x^^^2 = 0";
 
   491 "TODO 4 + x^^^2 = 0";
 
   491 "TODO 4 + x^^^2 = 0";
 
   492 "TODO 4 + x^^^2 = 0";
 
   492 
   493 
   493 "----- d2_pqformula10 ------";
 
   494 "----- d2_pqformula10 ------";
 
   497 (*val p = e_pos'; val c = []; 
   498 (*val p = e_pos'; val c = []; 
   498 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
 
   499 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
 
   499 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
 
   500 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
 
   500 
   501 
   501 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
 
   502 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
 
   502 val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   503 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
   503 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   504 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
   504 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   505 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
   505 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   506 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
   506 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   507 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
   507 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   508 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
   508 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   509 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
   509 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 2, x = -2]")) => ()
 
   510 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 2, x = -2]")) => ()
 
   510 	 | _ => error "polyeq.sml: diff.behav. in -4 + 1*x^2 = 0 -> [x = 2, x = -2]";
 
   511 	 | _ => error "polyeq.sml: diff.behav. in -4 + 1*x^2 = 0 -> [x = 2, x = -2]";
 
   511 
   512 
   512 "----- d2_pqformula9_neg ------";
 
   513 "----- d2_pqformula9_neg ------";
 
   513 val fmz = ["equality (4 + 1*x^^^2 = 0)", "solveFor x","solutions L"];
 
   514 val fmz = ["equality (4 + 1*x^^^2 = 0)", "solveFor x","solutions L"];
 
   516 (*val p = e_pos'; val c = []; 
   517 (*val p = e_pos'; val c = []; 
   517 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
 
   518 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
 
   518 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
 
   519 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
 
   519 
   520 
   520 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
 
   521 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
 
   521 val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   522 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
   522 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   523 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
   523 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   524 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
   524 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   525 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
   525 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   526 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
   526 val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   527 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
   527 "TODO 4 + 1*x^^^2 = 0";
 
   528 "TODO 4 + 1*x^^^2 = 0";
 
   528 "TODO 4 + 1*x^^^2 = 0";
 
   529 "TODO 4 + 1*x^^^2 = 0";
 
   529 "TODO 4 + 1*x^^^2 = 0";
 
   530 "TODO 4 + 1*x^^^2 = 0";
 
   530 
   531 
   531 "-------------------- test thm's d2_abc_formulsxx[_neg]-----";
 
   532 "-------------------- test thm's d2_abc_formulsxx[_neg]-----";
 
   538 (*val p = e_pos'; val c = []; 
   539 (*val p = e_pos'; val c = []; 
   539 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
 
   540 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
 
   540 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
 
   541 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
 
   541 
   542 
   542 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
 
   543 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
 
   543 val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   544 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
   544 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   545 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
   545 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   546 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
   546 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   547 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
   547 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   548 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
   548 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   549 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
   549 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   550 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
   550 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 1, x = -1 / 2]")) => ()
 
   551 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 1, x = -1 / 2]")) => ()
 
   551 	 | _ => error "polyeq.sml: diff.behav. in -1 + (-1)*x + 2*x^2 = 0 -> [x = 1, x = -1/2]";
 
   552 	 | _ => error "polyeq.sml: diff.behav. in -1 + (-1)*x + 2*x^2 = 0 -> [x = 1, x = -1/2]";
 
   552 
   553 
   553 val fmz = ["equality ( 1 +(-1)*x + 2*x^^^2 = 0)", "solveFor x","solutions L"];
 
   554 val fmz = ["equality ( 1 +(-1)*x + 2*x^^^2 = 0)", "solveFor x","solutions L"];
 
   554 val (dI',pI',mI') = ("PolyEq",["abcFormula","degree_2","polynomial","univariate","equation"],
 
   555 val (dI',pI',mI') = ("PolyEq",["abcFormula","degree_2","polynomial","univariate","equation"],
 
   556 (*val p = e_pos'; val c = []; 
   557 (*val p = e_pos'; val c = []; 
   557 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
 
   558 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
 
   558 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
 
   559 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
 
   559 
   560 
   560 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
 
   561 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
 
   561 val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   562 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
   562 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   563 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
   563 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   564 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
   564 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   565 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
   565 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   566 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
   566 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   567 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
   567 "TODO 1 +(-1)*x + 2*x^^^2 = 0";
 
   568 "TODO 1 +(-1)*x + 2*x^^^2 = 0";
 
   568 "TODO 1 +(-1)*x + 2*x^^^2 = 0";
 
   569 "TODO 1 +(-1)*x + 2*x^^^2 = 0";
 
   569 "TODO 1 +(-1)*x + 2*x^^^2 = 0";
 
   570 "TODO 1 +(-1)*x + 2*x^^^2 = 0";
 
   570 
   571 
   571 (*EP-11*)
 
   572 (*EP-11*)
 
   575 (*val p = e_pos'; val c = []; 
   576 (*val p = e_pos'; val c = []; 
   576 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
 
   577 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
 
   577 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
 
   578 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
 
   578 
   579 
   579 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
 
   580 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
 
   580 val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   581 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
   581 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   582 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
   582 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   583 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
   583 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   584 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
   584 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   585 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
   585 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   586 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
   586 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   587 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
   587 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 1 / 2, x = -1]")) => ()
 
   588 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 1 / 2, x = -1]")) => ()
 
   588 	 | _ => error "polyeq.sml: diff.behav. in -1 + x + 2*x^2 = 0 -> [x = 1/2, x = -1]";
 
   589 	 | _ => error "polyeq.sml: diff.behav. in -1 + x + 2*x^2 = 0 -> [x = 1/2, x = -1]";
 
   589 
   590 
   590 val fmz = ["equality ( 1 + x + 2*x^^^2 = 0)", "solveFor x","solutions L"];
 
   591 val fmz = ["equality ( 1 + x + 2*x^^^2 = 0)", "solveFor x","solutions L"];
 
   591 val (dI',pI',mI') = ("PolyEq",["abcFormula","degree_2","polynomial","univariate","equation"],
 
   592 val (dI',pI',mI') = ("PolyEq",["abcFormula","degree_2","polynomial","univariate","equation"],
 
   593 (*val p = e_pos'; val c = []; 
   594 (*val p = e_pos'; val c = []; 
   594 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
 
   595 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
 
   595 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
 
   596 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
 
   596 
   597 
   597 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
 
   598 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
 
   598 val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   599 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
   599 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   600 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
   600 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   601 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
   601 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   602 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
   602 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   603 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
   603 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   604 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
   604 val (p,_,f,nxt,_,pt) = me nxt p c pt; 
   605 val (p,_,f,nxt,_,pt) = me nxt p [] pt; 
   605 "TODO 1 + x + 2*x^^^2 = 0";
 
   606 "TODO 1 + x + 2*x^^^2 = 0";
 
   606 "TODO 1 + x + 2*x^^^2 = 0";
 
   607 "TODO 1 + x + 2*x^^^2 = 0";
 
   607 "TODO 1 + x + 2*x^^^2 = 0";
 
   608 "TODO 1 + x + 2*x^^^2 = 0";
 
   608 
   609 
   609 val fmz = ["equality (-2 + 1*x + x^^^2 = 0)", "solveFor x","solutions L"];
 
   610 val fmz = ["equality (-2 + 1*x + x^^^2 = 0)", "solveFor x","solutions L"];
 
   612 (*val p = e_pos'; val c = []; 
   613 (*val p = e_pos'; val c = []; 
   613 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
 
   614 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
 
   614 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
 
   615 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
 
   615 
   616 
   616 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
 
   617 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
 
   617 val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   618 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
   618 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   619 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
   619 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   620 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
   620 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   621 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
   621 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   622 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
   622 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   623 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
   623 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   624 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
   624 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 1, x = -2]")) => ()
 
   625 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 1, x = -2]")) => ()
 
   625 	 | _ => error "polyeq.sml: diff.behav. in -2 + 1*x + x^2 = 0 -> [x = 1, x = -2]";
 
   626 	 | _ => error "polyeq.sml: diff.behav. in -2 + 1*x + x^2 = 0 -> [x = 1, x = -2]";
 
   626 
   627 
   627 val fmz = ["equality ( 2 + 1*x + x^^^2 = 0)", "solveFor x","solutions L"];
 
   628 val fmz = ["equality ( 2 + 1*x + x^^^2 = 0)", "solveFor x","solutions L"];
 
   628 val (dI',pI',mI') = ("PolyEq",["abcFormula","degree_2","polynomial","univariate","equation"],
 
   629 val (dI',pI',mI') = ("PolyEq",["abcFormula","degree_2","polynomial","univariate","equation"],
 
   630 (*val p = e_pos'; val c = []; 
   631 (*val p = e_pos'; val c = []; 
   631 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
 
   632 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
 
   632 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
 
   633 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
 
   633 
   634 
   634 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
 
   635 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
 
   635 val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   636 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
   636 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   637 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
   637 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   638 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
   638 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   639 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
   639 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   640 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
   640 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   641 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
   641 val (p,_,f,nxt,_,pt) = me nxt p c pt; 
   642 val (p,_,f,nxt,_,pt) = me nxt p [] pt; 
   642 "TODO 2 + 1*x + x^^^2 = 0";
 
   643 "TODO 2 + 1*x + x^^^2 = 0";
 
   643 "TODO 2 + 1*x + x^^^2 = 0";
 
   644 "TODO 2 + 1*x + x^^^2 = 0";
 
   644 "TODO 2 + 1*x + x^^^2 = 0";
 
   645 "TODO 2 + 1*x + x^^^2 = 0";
 
   645 
   646 
   646 (*EP-12*)
 
   647 (*EP-12*)
 
   650 (*val p = e_pos'; val c = []; 
   651 (*val p = e_pos'; val c = []; 
   651 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
 
   652 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
 
   652 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
 
   653 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
 
   653 
   654 
   654 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
 
   655 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
 
   655 val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   656 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
   656 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   657 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
   657 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   658 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
   658 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   659 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
   659 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   660 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
   660 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   661 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
   661 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   662 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
   662 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 1, x = -2]")) => ()
 
   663 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 1, x = -2]")) => ()
 
   663 	 | _ => error "polyeq.sml: diff.behav. in -2 + x + x^2 = 0 -> [x = 1, x = -2]";
 
   664 	 | _ => error "polyeq.sml: diff.behav. in -2 + x + x^2 = 0 -> [x = 1, x = -2]";
 
   664 
   665 
   665 val fmz = ["equality ( 2 + x + x^^^2 = 0)", "solveFor x","solutions L"];
 
   666 val fmz = ["equality ( 2 + x + x^^^2 = 0)", "solveFor x","solutions L"];
 
   666 val (dI',pI',mI') = ("PolyEq",["abcFormula","degree_2","polynomial","univariate","equation"],
 
   667 val (dI',pI',mI') = ("PolyEq",["abcFormula","degree_2","polynomial","univariate","equation"],
 
   668 (*val p = e_pos'; val c = []; 
   669 (*val p = e_pos'; val c = []; 
   669 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
 
   670 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
 
   670 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
 
   671 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
 
   671 
   672 
   672 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
 
   673 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
 
   673 val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   674 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
   674 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   675 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
   675 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   676 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
   676 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   677 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
   677 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   678 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
   678 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   679 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
   679 val (p,_,f,nxt,_,pt) = me nxt p c pt; 
   680 val (p,_,f,nxt,_,pt) = me nxt p [] pt; 
   680 "TODO 2 + x + x^^^2 = 0";
 
   681 "TODO 2 + x + x^^^2 = 0";
 
   681 "TODO 2 + x + x^^^2 = 0";
 
   682 "TODO 2 + x + x^^^2 = 0";
 
   682 "TODO 2 + x + x^^^2 = 0";
 
   683 "TODO 2 + x + x^^^2 = 0";
 
   683 
   684 
   684 (*EP-13*)
 
   685 (*EP-13*)
 
   688 (*val p = e_pos'; val c = []; 
   689 (*val p = e_pos'; val c = []; 
   689 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
 
   690 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
 
   690 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
 
   691 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
 
   691 
   692 
   692 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
 
   693 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
 
   693 val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   694 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
   694 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   695 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
   695 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   696 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
   696 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   697 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
   697 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   698 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
   698 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   699 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
   699 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   700 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
   700 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 2, x = -2]")) => ()
 
   701 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 2, x = -2]")) => ()
 
   701 	 | _ => error "polyeq.sml: diff.behav. in -8 + 2*x^2 = 0 -> [x = 2, x = -2]";
 
   702 	 | _ => error "polyeq.sml: diff.behav. in -8 + 2*x^2 = 0 -> [x = 2, x = -2]";
 
   702 
   703 
   703 val fmz = ["equality ( 8+ 2*x^^^2 = 0)", "solveFor x","solutions L"];
 
   704 val fmz = ["equality ( 8+ 2*x^^^2 = 0)", "solveFor x","solutions L"];
 
   704 val (dI',pI',mI') = ("PolyEq",["abcFormula","degree_2","polynomial","univariate","equation"],
 
   705 val (dI',pI',mI') = ("PolyEq",["abcFormula","degree_2","polynomial","univariate","equation"],
 
   706 (*val p = e_pos'; val c = []; 
   707 (*val p = e_pos'; val c = []; 
   707 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
 
   708 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
 
   708 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
 
   709 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
 
   709 
   710 
   710 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
 
   711 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
 
   711 val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   712 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
   712 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   713 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
   713 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   714 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
   714 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   715 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
   715 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   716 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
   716 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   717 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
   717 "TODO 8+ 2*x^^^2 = 0";
 
   718 "TODO 8+ 2*x^^^2 = 0";
 
   718 "TODO 8+ 2*x^^^2 = 0";
 
   719 "TODO 8+ 2*x^^^2 = 0";
 
   719 "TODO 8+ 2*x^^^2 = 0";
 
   720 "TODO 8+ 2*x^^^2 = 0";
 
   720 
   721 
   721 (*EP-14*)
 
   722 (*EP-14*)
 
   724 (*val p = e_pos'; val c = []; 
   725 (*val p = e_pos'; val c = []; 
   725 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
 
   726 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
 
   726 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
 
   727 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
 
   727 
   728 
   728 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
 
   729 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
 
   729 val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   730 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
   730 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   731 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
   731 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   732 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
   732 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   733 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
   733 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   734 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
   734 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   735 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
   735 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   736 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
   736 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 2, x = -2]")) => ()
 
   737 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 2, x = -2]")) => ()
 
   737 	 | _ => error "polyeq.sml: diff.behav. in -4 + x^2 = 0 -> [x = 2, x = -2]";
 
   738 	 | _ => error "polyeq.sml: diff.behav. in -4 + x^2 = 0 -> [x = 2, x = -2]";
 
   738 
   739 
   739 
   740 
   740 val fmz = ["equality ( 4+ x^^^2 = 0)", "solveFor x","solutions L"];
 
   741 val fmz = ["equality ( 4+ x^^^2 = 0)", "solveFor x","solutions L"];
 
   742 (*val p = e_pos'; val c = []; 
   743 (*val p = e_pos'; val c = []; 
   743 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
 
   744 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
 
   744 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
 
   745 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
 
   745 
   746 
   746 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
 
   747 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
 
   747 val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   748 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
   748 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   749 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
   749 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   750 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
   750 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   751 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
   751 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   752 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
   752 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   753 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
   753 "TODO 4+ x^^^2 = 0";
 
   754 "TODO 4+ x^^^2 = 0";
 
   754 "TODO 4+ x^^^2 = 0";
 
   755 "TODO 4+ x^^^2 = 0";
 
   755 "TODO 4+ x^^^2 = 0";
 
   756 "TODO 4+ x^^^2 = 0";
 
   756 
   757 
   757 (*EP-15*)
 
   758 (*EP-15*)
 
   761 (*val p = e_pos'; val c = []; 
   762 (*val p = e_pos'; val c = []; 
   762 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
 
   763 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
 
   763 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
 
   764 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
 
   764 
   765 
   765 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
 
   766 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
 
   766 val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   767 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
   767 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   768 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
   768 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   769 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
   769 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   770 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
   770 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   771 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
   771 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   772 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
   772 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   773 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
   773 case f of Form' (FormKF (~1,EdUndef,_,Nundef,"[x = 0, x = -1]")) => ()
 
   774 case f of Form' (FormKF (~1,EdUndef,_,Nundef,"[x = 0, x = -1]")) => ()
 
   774 	 | _ => error "polyeq.sml: diff.behav. in x + x^2 = 0 -> [x = 0, x = -1]";
 
   775 	 | _ => error "polyeq.sml: diff.behav. in x + x^2 = 0 -> [x = 0, x = -1]";
 
   775 
   776 
   776 val fmz = ["equality (1*x + x^^^2 = 0)", "solveFor x","solutions L"];
 
   777 val fmz = ["equality (1*x + x^^^2 = 0)", "solveFor x","solutions L"];
 
   777 val (dI',pI',mI') = ("PolyEq",["abcFormula","degree_2","polynomial","univariate","equation"],
 
   778 val (dI',pI',mI') = ("PolyEq",["abcFormula","degree_2","polynomial","univariate","equation"],
 
   779 (*val p = e_pos'; val c = []; 
   780 (*val p = e_pos'; val c = []; 
   780 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
 
   781 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
 
   781 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
 
   782 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
 
   782 
   783 
   783 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
 
   784 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
 
   784 val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   785 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
   785 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   786 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
   786 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   787 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
   787 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   788 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
   788 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   789 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
   789 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   790 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
   790 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   791 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
   791 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 0, x = -1]")) => ()
 
   792 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 0, x = -1]")) => ()
 
   792 	 | _ => error "polyeq.sml: diff.behav. in x + x^2 = 0 -> [x = 0, x = -1]";
 
   793 	 | _ => error "polyeq.sml: diff.behav. in x + x^2 = 0 -> [x = 0, x = -1]";
 
   793 
   794 
   794 (*EP-16*)
 
   795 (*EP-16*)
 
   795 val fmz = ["equality (x + 2*x^^^2 = 0)", "solveFor x","solutions L"];
 
   796 val fmz = ["equality (x + 2*x^^^2 = 0)", "solveFor x","solutions L"];
 
   798 (*val p = e_pos'; val c = []; 
   799 (*val p = e_pos'; val c = []; 
   799 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
 
   800 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
 
   800 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
 
   801 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
 
   801 
   802 
   802 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
 
   803 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
 
   803 val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   804 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
   804 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   805 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
   805 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   806 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
   806 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   807 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
   807 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   808 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
   808 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   809 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
   809 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   810 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
   810 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 0, x = -1 / 2]")) => ()
 
   811 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 0, x = -1 / 2]")) => ()
 
   811 	 | _ => error "polyeq.sml: diff.behav. in x + x^2 = 0 -> [x = 0, x = -1 / 2]";
 
   812 	 | _ => error "polyeq.sml: diff.behav. in x + x^2 = 0 -> [x = 0, x = -1 / 2]";
 
   812 
   813 
   813 (*EP-//*)
 
   814 (*EP-//*)
 
   814 val fmz = ["equality (x + x^^^2 = 0)", "solveFor x","solutions L"];
 
   815 val fmz = ["equality (x + x^^^2 = 0)", "solveFor x","solutions L"];
 
   817 (*val p = e_pos'; val c = []; 
   818 (*val p = e_pos'; val c = []; 
   818 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
 
   819 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
 
   819 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
 
   820 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
 
   820 
   821 
   821 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
 
   822 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
 
   822 val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   823 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
   823 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   824 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
   824 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   825 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
   825 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   826 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
   826 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   827 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
   827 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   828 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
   828 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   829 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
   829 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 0, x = -1]")) => ()
 
   830 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 0, x = -1]")) => ()
 
   830 	 | _ => error "polyeq.sml: diff.behav. in x + x^2 = 0 -> [x = 0, x = -1]";
 
   831 	 | _ => error "polyeq.sml: diff.behav. in x + x^2 = 0 -> [x = 0, x = -1]";
 
   831 
   832 
   832 "----------- (-8 - 2*x + x^^^2 = 0),  (*Schalk 2, S.67 Nr.31.b----";
 
   833 "----------- (-8 - 2*x + x^^^2 = 0),  (*Schalk 2, S.67 Nr.31.b----";
 
   833 "----------- (-8 - 2*x + x^^^2 = 0),  (*Schalk 2, S.67 Nr.31.b----";
 
   834 "----------- (-8 - 2*x + x^^^2 = 0),  (*Schalk 2, S.67 Nr.31.b----";
 
   840 (* val p = e_pos'; val c = []; 
   841 (* val p = e_pos'; val c = []; 
   841  val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
 
   842  val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
 
   842  val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
 
   843  val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
 
   843 
   844 
   844 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
 
   845 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
 
   845 val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   846 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
   846  val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   847  val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
   847  val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   848  val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
   848  val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   849  val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
   849  (*Apply_Method ("PolyEq","complete_square")*)
 
   850  (*Apply_Method ("PolyEq","complete_square")*)
 
   850  val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   851  val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
   851  (*"-8 - 2 * x + x ^^^ 2 = 0", nxt = Rewrite_Set_Inst ... "complete_square*)
 
   852  (*"-8 - 2 * x + x ^^^ 2 = 0", nxt = Rewrite_Set_Inst ... "complete_square*)
 
   852  val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   853  val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
   853  (*"-8 + (2 / 2 - x) ^^^ 2 = (2 / 2) ^^^ 2", nxt = Rewrite("square_explicit1"*)
 
   854  (*"-8 + (2 / 2 - x) ^^^ 2 = (2 / 2) ^^^ 2", nxt = Rewrite("square_explicit1"*)
 
   854  val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   855  val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
   855  (*"(2 / 2 - x) ^^^ 2 = (2 / 2) ^^^ 2 - -8" nxt = Rewrite("root_plus_minus*)
 
   856  (*"(2 / 2 - x) ^^^ 2 = (2 / 2) ^^^ 2 - -8" nxt = Rewrite("root_plus_minus*)
 
   856  val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   857  val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
   857  (*"2 / 2 - x = sqrt ((2 / 2) ^^^ 2 - -8) |
 
   858  (*"2 / 2 - x = sqrt ((2 / 2) ^^^ 2 - -8) |
 
   858     2 / 2 - x = - sqrt ((2 / 2) ^^^ 2 - -8)" nxt = Rewr_Inst("bdv_explicit2"*)
 
   859     2 / 2 - x = - sqrt ((2 / 2) ^^^ 2 - -8)" nxt = Rewr_Inst("bdv_explicit2"*)
 
   859  val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   860  val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
   860  (*"2 / 2 - x = sqrt ((2 / 2) ^^^ 2 - -8) |
 
   861  (*"2 / 2 - x = sqrt ((2 / 2) ^^^ 2 - -8) |
 
   861     -1*x = - (2 / 2) + - sqrt ((2 / 2) ^^^ 2 - -8)"nxt = R_Inst("bdv_explt2"*)
 
   862     -1*x = - (2 / 2) + - sqrt ((2 / 2) ^^^ 2 - -8)"nxt = R_Inst("bdv_explt2"*)
 
   862  val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   863  val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
   863  (*"-1 * x = - (2 / 2) + sqrt ((2 / 2) ^^^ 2 - -8) |
 
   864  (*"-1 * x = - (2 / 2) + sqrt ((2 / 2) ^^^ 2 - -8) |
 
   864     -1 * x = (- (2 / 2) + - sqrt ((2 / 2) ^^^ 2 - -8))"nxt = bdv_explicit3*)
 
   865     -1 * x = (- (2 / 2) + - sqrt ((2 / 2) ^^^ 2 - -8))"nxt = bdv_explicit3*)
 
   865  val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   866  val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
   866  (*"-1 * x = - (2 / 2) + sqrt ((2 / 2) ^^^ 2 - -8) |
 
   867  (*"-1 * x = - (2 / 2) + sqrt ((2 / 2) ^^^ 2 - -8) |
 
   867    x = -1 * (- (2 / 2) + - sqrt ((2 / 2) ^^^ 2 - -8))" nxt = bdv_explicit3*)
 
   868    x = -1 * (- (2 / 2) + - sqrt ((2 / 2) ^^^ 2 - -8))" nxt = bdv_explicit3*)
 
   868  val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   869  val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
   869  (*"x = -1 * (- (2 / 2) + sqrt ((2 / 2) ^^^ 2 - -8)) |
 
   870  (*"x = -1 * (- (2 / 2) + sqrt ((2 / 2) ^^^ 2 - -8)) |
 
   870     x = -1 * (- (2 / 2) + - sqrt ((2 / 2) ^^^ 2 - -8))"nxt = calculate_Ration*)
 
   871     x = -1 * (- (2 / 2) + - sqrt ((2 / 2) ^^^ 2 - -8))"nxt = calculate_Ration*)
 
   871  val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   872  val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
   872  (*"x = -2 | x = 4" nxt = Or_to_List*)
 
   873  (*"x = -2 | x = 4" nxt = Or_to_List*)
 
   873  val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   874  val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
   874  (*"[x = -2, x = 4]" nxt = Check_Postcond*)
 
   875  (*"[x = -2, x = 4]" nxt = Check_Postcond*)
 
   875  val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
 
   876  val (p,_,f,nxt,_,pt) = me nxt p [] pt; f2str f;
 
   876 (* FIXXXME 
   877 (* FIXXXME 
   877  case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = -2, x = 4]")) => () TODO
 
   878  case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = -2, x = 4]")) => () TODO
 
   878 	 | _ => error "polyeq.sml: diff.behav. in [x = -2, x = 4]";
 
   879 	 | _ => error "polyeq.sml: diff.behav. in [x = -2, x = 4]";
 
   879 *)
 
   880 *)
 
   880 if f2str f = "[x = -1 * -1 + -1 * sqrt (1 ^^^ 2 - -8),\n x = -1 * -1 + -1 * (-1 * sqrt (1 ^^^ 2 - -8))]" then ()
 
   881 if f2str f = "[x = -1 * -1 + -1 * sqrt (1 ^^^ 2 - -8),\n x = -1 * -1 + -1 * (-1 * sqrt (1 ^^^ 2 - -8))]" then ()
 
   899 (* val p = e_pos'; val c = []; 
   900 (* val p = e_pos'; val c = []; 
   900  val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
 
   901  val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
 
   901  val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
 
   902  val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
 
   902 
   903 
   903 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
 
   904 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
 
   904 val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   905 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
   905  val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   906  val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
   906  val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   907  val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
   907  val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   908  val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
   908  val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   909  val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
   909  val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   910  val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
   910  val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   911  val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
   911  (*Apply_Method ("PolyEq","complete_square")*)
 
   912  (*Apply_Method ("PolyEq","complete_square")*)
 
   912  val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
 
   913  val (p,_,f,nxt,_,pt) = me nxt p [] pt; f2str f;
 
   913 
   914 
   914 "----------- (-16 + 4*x + 2*x^^^2 = 0), --------------------------";
 
   915 "----------- (-16 + 4*x + 2*x^^^2 = 0), --------------------------";
 
   915 "----------- (-16 + 4*x + 2*x^^^2 = 0), --------------------------";
 
   916 "----------- (-16 + 4*x + 2*x^^^2 = 0), --------------------------";
 
   916 "----------- (-16 + 4*x + 2*x^^^2 = 0), --------------------------";
 
   917 "----------- (-16 + 4*x + 2*x^^^2 = 0), --------------------------";
 
   917  val fmz = ["equality (-16 + 4*x + 2*x^^^2 = 0)",
 
   918  val fmz = ["equality (-16 + 4*x + 2*x^^^2 = 0)",
 
   922 (* val p = e_pos'; val c = []; 
   923 (* val p = e_pos'; val c = []; 
   923  val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
 
   924  val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
 
   924  val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*) 
   925  val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*) 
   925 
   926 
   926 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
 
   927 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
 
   927 val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   928 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
   928  val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   929  val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
   929  val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   930  val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
   930  val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   931  val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
   931  val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   932  val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
   932  val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   933  val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
   933  val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   934  val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
   934  (*Apply_Method ("PolyEq","complete_square")*)
 
   935  (*Apply_Method ("PolyEq","complete_square")*)
 
   935  val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   936  val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
   936  val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   937  val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
   937  val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   938  val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
   938  val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   939  val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
   939  val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   940  val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
   940  val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   941  val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
   941  val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   942  val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
   942  val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   943  val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
   943  val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   944  val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
   944  val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   945  val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
   945 (* FIXXXXME n1.,
 
   946 (* FIXXXXME n1.,
 
   946  case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 2, x = -4]")) => () TODO
 
   947  case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 2, x = -4]")) => () TODO
 
   947 	 | _ => error "polyeq.sml: diff.behav. in [x = 2, x = -4]";
 
   948 	 | _ => error "polyeq.sml: diff.behav. in [x = 2, x = -4]";
 
   948 *)
 
   949 *)
 
   949 
   950 
   958 (* val p = e_pos'; val c = []; 
   959 (* val p = e_pos'; val c = []; 
   959  val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
 
   960  val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
 
   960  val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
 
   961  val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
 
   961 
   962 
   962 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
 
   963 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
 
   963 val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   964 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
   964  val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   965  val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
   965  val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   966  val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
   966  val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   967  val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
   967  val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   968  val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
   968  val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   969  val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
   969  val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   970  val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
   970  val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   971  val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
   971  val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   972  val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
   972  val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   973  val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
   973 
   974 
   974  val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   975  val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
   975  val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   976  val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
   976  val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   977  val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
   977  val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   978  val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
   978  val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   979  val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
   979  val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   980  val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
   980  val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   981  val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
   981  val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
 
   982  val (p,_,f,nxt,_,pt) = me nxt p [] pt; f2str f;
 
   982 (*WN.2.5.03 TODO FIXME Matthias ?
 
   983 (*WN.2.5.03 TODO FIXME Matthias ?
 
   983  case f of 
   984  case f of 
   984      Form' 
   985      Form' 
   985 	 (FormKF 
   986 	 (FormKF 
   986 	      (~1,EdUndef,0,Nundef,
 
   987 	      (~1,EdUndef,0,Nundef,
 
  1001 (* val p = e_pos'; val c = []; 
  1002 (* val p = e_pos'; val c = []; 
  1002  val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
 
  1003  val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
 
  1003  val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
 
  1004  val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
 
  1004 
  1005 
  1005 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
 
  1006 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
 
  1006 val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
  1007 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
  1007  val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
  1008  val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
  1008  val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
  1009  val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
  1009  val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
  1010  val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
  1010  val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
  1011  val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
  1011  val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
  1012  val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
  1012  val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
  1013  val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
  1013  val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
  1014  val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
  1014  val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
  1015  val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
  1015  val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
  1016  val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
  1016  val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
  1017  val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
  1017  val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
  1018  val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
  1018  val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
 
  1019  val (p,_,f,nxt,_,pt) = me nxt p [] pt; f2str f;
 
  1019 (*WN.2.5.03 TODO "[x = sqrt (0 - -64), x = -1 * sqrt (0 - -64)]"
 
  1020 (*WN.2.5.03 TODO "[x = sqrt (0 - -64), x = -1 * sqrt (0 - -64)]"
 
  1020  case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 8, x = -8]")) => ()
 
  1021  case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 8, x = -8]")) => ()
 
  1021 	 | _ => error "polyeq.sml: diff.behav. in [x = 8, x = -8]";
 
  1022 	 | _ => error "polyeq.sml: diff.behav. in [x = 8, x = -8]";
 
  1022 *)
 
  1023 *)
 
  1023 
  1024 
  1032 (* val p = e_pos'; val c = []; 
  1033 (* val p = e_pos'; val c = []; 
  1033  val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
 
  1034  val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
 
  1034  val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
 
  1035  val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
 
  1035 
  1036 
  1036 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
 
  1037 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
 
  1037 val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
  1038 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
  1038  val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
  1039  val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
  1039  val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
  1040  val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
  1040  val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
  1041  val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
  1041  val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
  1042  val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
  1042  val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
  1043  val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
  1043  val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
  1044  val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
  1044  val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
  1045  val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
  1045 (*WN.2.5.03 TODO "[x = sqrt (0 - -49), x = -1 * sqrt (0 - -49)]"
 
  1046 (*WN.2.5.03 TODO "[x = sqrt (0 - -49), x = -1 * sqrt (0 - -49)]"
 
  1046  case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 7, x = -7]")) => ()
 
  1047  case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 7, x = -7]")) => ()
 
  1047 	 | _ => error "polyeq.sml: diff.behav. in [x = 7, x = -7]";
 
  1048 	 | _ => error "polyeq.sml: diff.behav. in [x = 7, x = -7]";
 
  1048 *)
 
  1049 *)
 
  1049 if f2str f = "[x = sqrt (0 - -49), x = -1 * sqrt (0 - -49)]" then ()
 
  1050 if f2str f = "[x = sqrt (0 - -49), x = -1 * sqrt (0 - -49)]" then ()
wneuper/isa