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
branchisac-update-Isa09-2
changeset 37991 028442673981
parent 37960 ec20007095f2
child 38031 460c24a6a6ba
equal deleted inserted replaced
37990:24609758d219 37991:028442673981 
   123 "-------------------- test thm's degree_0 --------------------------------------";
 
   123 "-------------------- test thm's degree_0 --------------------------------------";
 
   124 "-------------------- test thm's degree_0 --------------------------------------";
 
   124 "-------------------- test thm's degree_0 --------------------------------------";
 
   125 "----- d0_false ------";
 
   125 "----- d0_false ------";
 
   126 (*EP*)
 
   126 (*EP*)
 
   127 val fmz = ["equality ( 1 = 0)", "solveFor x","solutions L"];
 
   127 val fmz = ["equality ( 1 = 0)", "solveFor x","solutions L"];
 
   128 val (dI',pI',mI') = ("PolyEq.thy",["degree_0","polynomial","univariate","equation"],
 
   128 val (dI',pI',mI') = ("PolyEq",["degree_0","polynomial","univariate","equation"],
 
   129                      ["PolyEq","solve_d0_polyeq_equation"]);
 
   129                      ["PolyEq","solve_d0_polyeq_equation"]);
 
   130 (*val p = e_pos'; 
   130 (*val p = e_pos'; 
   131 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
 
   131 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
 
   132 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
 
   132 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
 
   133 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
 
   133 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
 
   141 	 | _ => raise error "polyeq.sml: diff.behav. in 1 = 0 -> []";
 
   141 	 | _ => raise error "polyeq.sml: diff.behav. in 1 = 0 -> []";
 
   142 
   142 
   143 "----- d0_true ------";
 
   143 "----- d0_true ------";
 
   144 (*EP-7*)
 
   144 (*EP-7*)
 
   145 val fmz = ["equality ( 0 = 0)", "solveFor x","solutions L"];
 
   145 val fmz = ["equality ( 0 = 0)", "solveFor x","solutions L"];
 
   146 val (dI',pI',mI') = ("PolyEq.thy",["degree_0","polynomial","univariate","equation"],
 
   146 val (dI',pI',mI') = ("PolyEq",["degree_0","polynomial","univariate","equation"],
 
   147                      ["PolyEq","solve_d0_polyeq_equation"]);
 
   147                      ["PolyEq","solve_d0_polyeq_equation"]);
 
   148 (*val p = e_pos'; val c = []; 
   148 (*val p = e_pos'; val c = []; 
   149 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
 
   149 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
 
   150 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
 
   150 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
 
   151 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
 
   151 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
 
   165 "-------------------- test thm's d2_pq_formulsxx[_neg]-----";
 
   165 "-------------------- test thm's d2_pq_formulsxx[_neg]-----";
 
   166 "-------------------- test thm's d2_pq_formulsxx[_neg]-----";
 
   166 "-------------------- test thm's d2_pq_formulsxx[_neg]-----";
 
   167 
   167 
   168 "----- d2_pqformula1 ------!!!!";
 
   168 "----- d2_pqformula1 ------!!!!";
 
   169 val fmz = ["equality (-2 +(-1)*x + x^^^2 = 0)", "solveFor x","solutions L"];
 
   169 val fmz = ["equality (-2 +(-1)*x + x^^^2 = 0)", "solveFor x","solutions L"];
 
   170 val (dI',pI',mI') = ("PolyEq.thy",["pqFormula","degree_2","polynomial","univariate","equation"], ["PolyEq","solve_d2_polyeq_pq_equation"]);
 
   170 val (dI',pI',mI') = ("PolyEq",["pqFormula","degree_2","polynomial","univariate","equation"], ["PolyEq","solve_d2_polyeq_pq_equation"]);
 
   171 (*val p = e_pos'; val c = []; 
   171 (*val p = e_pos'; val c = []; 
   172 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
 
   172 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
 
   173 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
 
   173 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
 
   174 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
 
   174 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
 
   175 val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   175 val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   192 	 | _ => raise error "polyeq.sml: diff.behav. in -2 + (-1)*x + x^2 = 0 -> [x = 2, x = -1]";
 
   192 	 | _ => raise error "polyeq.sml: diff.behav. in -2 + (-1)*x + x^2 = 0 -> [x = 2, x = -1]";
 
   193 
   193 
   194 "----- d2_pqformula1_neg ------";
 
   194 "----- d2_pqformula1_neg ------";
 
   195 (*EP-8*)
 
   195 (*EP-8*)
 
   196 val fmz = ["equality ( 2 +(-1)*x + x^^^2 = 0)", "solveFor x","solutions L"];
 
   196 val fmz = ["equality ( 2 +(-1)*x + x^^^2 = 0)", "solveFor x","solutions L"];
 
   197 val (dI',pI',mI') = ("PolyEq.thy",["pqFormula","degree_2","polynomial","univariate","equation"], ["PolyEq","solve_d2_polyeq_pq_equation"]);
 
   197 val (dI',pI',mI') = ("PolyEq",["pqFormula","degree_2","polynomial","univariate","equation"], ["PolyEq","solve_d2_polyeq_pq_equation"]);
 
   198 (*val p = e_pos'; val c = []; 
   198 (*val p = e_pos'; val c = []; 
   199 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
 
   199 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
 
   200 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
 
   200 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
 
   201 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
 
   201 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
 
   202 val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   202 val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   215 if f = Form' (FormKF (~1,EdUndef,0,Nundef,"[]")) andalso asm = [] then ()
 
   215 if f = Form' (FormKF (~1,EdUndef,0,Nundef,"[]")) andalso asm = [] then ()
 
   216 else raise error "polyeq.sml: diff.behav. in 2 +(-1)*x + x^^^2 = 0";
 
   216 else raise error "polyeq.sml: diff.behav. in 2 +(-1)*x + x^^^2 = 0";
 
   217 
   217 
   218 "----- d2_pqformula2 ------";
 
   218 "----- d2_pqformula2 ------";
 
   219 val fmz = ["equality (-2 +(-1)*x + 1*x^^^2 = 0)", "solveFor x","solutions L"];
 
   219 val fmz = ["equality (-2 +(-1)*x + 1*x^^^2 = 0)", "solveFor x","solutions L"];
 
   220 val (dI',pI',mI') = ("PolyEq.thy",["pqFormula","degree_2","polynomial","univariate","equation"],
 
   220 val (dI',pI',mI') = ("PolyEq",["pqFormula","degree_2","polynomial","univariate","equation"],
 
   221                      ["PolyEq","solve_d2_polyeq_pq_equation"]);
 
   221                      ["PolyEq","solve_d2_polyeq_pq_equation"]);
 
   222 (*val p = e_pos'; val c = []; 
   222 (*val p = e_pos'; val c = []; 
   223 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
 
   223 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
 
   224 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
 
   224 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
 
   225 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
 
   225 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
 
   235 	 | _ => raise error "polyeq.sml: diff.behav. in -2 + (-1)*x + x^2 = 0 -> [x = 2, x = -1]";
 
   235 	 | _ => raise error "polyeq.sml: diff.behav. in -2 + (-1)*x + x^2 = 0 -> [x = 2, x = -1]";
 
   236 
   236 
   237 
   237 
   238 "----- d2_pqformula2_neg ------";
 
   238 "----- d2_pqformula2_neg ------";
 
   239 val fmz = ["equality ( 2 +(-1)*x + 1*x^^^2 = 0)", "solveFor x","solutions L"];
 
   239 val fmz = ["equality ( 2 +(-1)*x + 1*x^^^2 = 0)", "solveFor x","solutions L"];
 
   240 val (dI',pI',mI') = ("PolyEq.thy",["pqFormula","degree_2","polynomial","univariate","equation"],
 
   240 val (dI',pI',mI') = ("PolyEq",["pqFormula","degree_2","polynomial","univariate","equation"],
 
   241                      ["PolyEq","solve_d2_polyeq_pq_equation"]);
 
   241                      ["PolyEq","solve_d2_polyeq_pq_equation"]);
 
   242 (*val p = e_pos'; val c = []; 
   242 (*val p = e_pos'; val c = []; 
   243 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
 
   243 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
 
   244 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
 
   244 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
 
   245 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
 
   245 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
 
   256 
   256 
   257 
   257 
   258 "----- d2_pqformula3 ------";
 
   258 "----- d2_pqformula3 ------";
 
   259 (*EP-9*)
 
   259 (*EP-9*)
 
   260 val fmz = ["equality (-2 + x + x^^^2 = 0)", "solveFor x","solutions L"];
 
   260 val fmz = ["equality (-2 + x + x^^^2 = 0)", "solveFor x","solutions L"];
 
   261 val (dI',pI',mI') = ("PolyEq.thy",["pqFormula","degree_2","polynomial","univariate","equation"],
 
   261 val (dI',pI',mI') = ("PolyEq",["pqFormula","degree_2","polynomial","univariate","equation"],
 
   262                      ["PolyEq","solve_d2_polyeq_pq_equation"]);
 
   262                      ["PolyEq","solve_d2_polyeq_pq_equation"]);
 
   263 (*val p = e_pos'; val c = []; 
   263 (*val p = e_pos'; val c = []; 
   264 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
 
   264 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
 
   265 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
 
   265 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
 
   266 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
 
   266 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
 
   275 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 1, x = -2]")) => ()
 
   275 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 1, x = -2]")) => ()
 
   276 	 | _ => raise error "polyeq.sml: diff.behav. in  -2 + x + x^2 = 0-> [x = 1, x = -2]";
 
   276 	 | _ => raise error "polyeq.sml: diff.behav. in  -2 + x + x^2 = 0-> [x = 1, x = -2]";
 
   277 
   277 
   278 "----- d2_pqformula3_neg ------";
 
   278 "----- d2_pqformula3_neg ------";
 
   279 val fmz = ["equality ( 2 + x + x^^^2 = 0)", "solveFor x","solutions L"];
 
   279 val fmz = ["equality ( 2 + x + x^^^2 = 0)", "solveFor x","solutions L"];
 
   280 val (dI',pI',mI') = ("PolyEq.thy",["pqFormula","degree_2","polynomial","univariate","equation"],
 
   280 val (dI',pI',mI') = ("PolyEq",["pqFormula","degree_2","polynomial","univariate","equation"],
 
   281                      ["PolyEq","solve_d2_polyeq_pq_equation"]);
 
   281                      ["PolyEq","solve_d2_polyeq_pq_equation"]);
 
   282 (*val p = e_pos'; val c = []; 
   282 (*val p = e_pos'; val c = []; 
   283 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
 
   283 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
 
   284 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
 
   284 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
 
   285 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
 
   285 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
 
   295 "TODO 2 + x + x^^^2 = 0";
 
   295 "TODO 2 + x + x^^^2 = 0";
 
   296 
   296 
   297 
   297 
   298 "----- d2_pqformula4 ------";
 
   298 "----- d2_pqformula4 ------";
 
   299 val fmz = ["equality (-2 + x + 1*x^^^2 = 0)", "solveFor x","solutions L"];
 
   299 val fmz = ["equality (-2 + x + 1*x^^^2 = 0)", "solveFor x","solutions L"];
 
   300 val (dI',pI',mI') = ("PolyEq.thy",["pqFormula","degree_2","polynomial","univariate","equation"],
 
   300 val (dI',pI',mI') = ("PolyEq",["pqFormula","degree_2","polynomial","univariate","equation"],
 
   301                      ["PolyEq","solve_d2_polyeq_pq_equation"]);
 
   301                      ["PolyEq","solve_d2_polyeq_pq_equation"]);
 
   302 (*val p = e_pos'; val c = []; 
   302 (*val p = e_pos'; val c = []; 
   303 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
 
   303 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
 
   304 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
 
   304 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
 
   305 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
 
   305 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
 
   314 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 1, x = -2]")) => ()
 
   314 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 1, x = -2]")) => ()
 
   315 	 | _ => raise error "polyeq.sml: diff.behav. in  -2 + x + 1*x^^^2 = 0 -> [x = 1, x = -2]";
 
   315 	 | _ => raise error "polyeq.sml: diff.behav. in  -2 + x + 1*x^^^2 = 0 -> [x = 1, x = -2]";
 
   316 
   316 
   317 "----- d2_pqformula4_neg ------";
 
   317 "----- d2_pqformula4_neg ------";
 
   318 val fmz = ["equality ( 2 + x + 1*x^^^2 = 0)", "solveFor x","solutions L"];
 
   318 val fmz = ["equality ( 2 + x + 1*x^^^2 = 0)", "solveFor x","solutions L"];
 
   319 val (dI',pI',mI') = ("PolyEq.thy",["pqFormula","degree_2","polynomial","univariate","equation"],
 
   319 val (dI',pI',mI') = ("PolyEq",["pqFormula","degree_2","polynomial","univariate","equation"],
 
   320                      ["PolyEq","solve_d2_polyeq_pq_equation"]);
 
   320                      ["PolyEq","solve_d2_polyeq_pq_equation"]);
 
   321 (*val p = e_pos'; val c = []; 
   321 (*val p = e_pos'; val c = []; 
   322 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
 
   322 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
 
   323 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
 
   323 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
 
   324 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
 
   324 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
 
   332 "TODO 2 + x + 1*x^^^2 = 0";
 
   332 "TODO 2 + x + 1*x^^^2 = 0";
 
   333 "TODO 2 + x + 1*x^^^2 = 0";
 
   333 "TODO 2 + x + 1*x^^^2 = 0";
 
   334 
   334 
   335 "----- d2_pqformula5 ------";
 
   335 "----- d2_pqformula5 ------";
 
   336 val fmz = ["equality (1*x +   x^^^2 = 0)", "solveFor x","solutions L"];
 
   336 val fmz = ["equality (1*x +   x^^^2 = 0)", "solveFor x","solutions L"];
 
   337 val (dI',pI',mI') = ("PolyEq.thy",["pqFormula","degree_2","polynomial","univariate","equation"],
 
   337 val (dI',pI',mI') = ("PolyEq",["pqFormula","degree_2","polynomial","univariate","equation"],
 
   338                      ["PolyEq","solve_d2_polyeq_pq_equation"]);
 
   338                      ["PolyEq","solve_d2_polyeq_pq_equation"]);
 
   339 (*val p = e_pos'; val c = []; 
   339 (*val p = e_pos'; val c = []; 
   340 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
 
   340 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
 
   341 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
 
   341 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
 
   342 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
 
   342 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
 
   351 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 0, x = -1]")) => ()
 
   351 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 0, x = -1]")) => ()
 
   352 	 | _ => raise error "polyeq.sml: diff.behav. in  1*x +   x^2 = 0 -> [x = 0, x = -1]";
 
   352 	 | _ => raise error "polyeq.sml: diff.behav. in  1*x +   x^2 = 0 -> [x = 0, x = -1]";
 
   353 
   353 
   354 "----- d2_pqformula6 ------";
 
   354 "----- d2_pqformula6 ------";
 
   355 val fmz = ["equality (1*x + 1*x^^^2 = 0)", "solveFor x","solutions L"];
 
   355 val fmz = ["equality (1*x + 1*x^^^2 = 0)", "solveFor x","solutions L"];
 
   356 val (dI',pI',mI') = ("PolyEq.thy",["pqFormula","degree_2","polynomial","univariate","equation"],
 
   356 val (dI',pI',mI') = ("PolyEq",["pqFormula","degree_2","polynomial","univariate","equation"],
 
   357                      ["PolyEq","solve_d2_polyeq_pq_equation"]);
 
   357                      ["PolyEq","solve_d2_polyeq_pq_equation"]);
 
   358 (*val p = e_pos'; val c = []; 
   358 (*val p = e_pos'; val c = []; 
   359 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
 
   359 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
 
   360 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
 
   360 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
 
   361 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
 
   361 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
 
   371 	 | _ => raise error "polyeq.sml: diff.behav. in  1*x + 1*x^2 = 0 -> [x = 0, x = -1]";
 
   371 	 | _ => raise error "polyeq.sml: diff.behav. in  1*x + 1*x^2 = 0 -> [x = 0, x = -1]";
 
   372 
   372 
   373 "----- d2_pqformula7 ------";
 
   373 "----- d2_pqformula7 ------";
 
   374 (*EP-10*)
 
   374 (*EP-10*)
 
   375 val fmz = ["equality (  x +   x^^^2 = 0)", "solveFor x","solutions L"];
 
   375 val fmz = ["equality (  x +   x^^^2 = 0)", "solveFor x","solutions L"];
 
   376 val (dI',pI',mI') = ("PolyEq.thy",["pqFormula","degree_2","polynomial","univariate","equation"],
 
   376 val (dI',pI',mI') = ("PolyEq",["pqFormula","degree_2","polynomial","univariate","equation"],
 
   377                      ["PolyEq","solve_d2_polyeq_pq_equation"]);
 
   377                      ["PolyEq","solve_d2_polyeq_pq_equation"]);
 
   378 (*val p = e_pos'; val c = []; 
   378 (*val p = e_pos'; val c = []; 
   379 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
 
   379 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
 
   380 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
 
   380 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
 
   381 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
 
   381 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
 
   390 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 0, x = -1]")) => ()
 
   390 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 0, x = -1]")) => ()
 
   391 	 | _ => raise error "polyeq.sml: diff.behav. in  x + x^2 = 0 -> [x = 0, x = -1]";
 
   391 	 | _ => raise error "polyeq.sml: diff.behav. in  x + x^2 = 0 -> [x = 0, x = -1]";
 
   392 
   392 
   393 "----- d2_pqformula8 ------";
 
   393 "----- d2_pqformula8 ------";
 
   394 val fmz = ["equality (  x + 1*x^^^2 = 0)", "solveFor x","solutions L"];
 
   394 val fmz = ["equality (  x + 1*x^^^2 = 0)", "solveFor x","solutions L"];
 
   395 val (dI',pI',mI') = ("PolyEq.thy",["pqFormula","degree_2","polynomial","univariate","equation"],
 
   395 val (dI',pI',mI') = ("PolyEq",["pqFormula","degree_2","polynomial","univariate","equation"],
 
   396                      ["PolyEq","solve_d2_polyeq_pq_equation"]);
 
   396                      ["PolyEq","solve_d2_polyeq_pq_equation"]);
 
   397 (*val p = e_pos'; val c = []; 
   397 (*val p = e_pos'; val c = []; 
   398 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
 
   398 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
 
   399 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
 
   399 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
 
   400 
   400 
   410 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 0, x = -1]")) => ()
 
   410 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 0, x = -1]")) => ()
 
   411 	 | _ => raise error "polyeq.sml: diff.behav. in  x + 1*x^2 = 0 -> [x = 0, x = -1]";
 
   411 	 | _ => raise error "polyeq.sml: diff.behav. in  x + 1*x^2 = 0 -> [x = 0, x = -1]";
 
   412 
   412 
   413 "----- d2_pqformula9 ------";
 
   413 "----- d2_pqformula9 ------";
 
   414 val fmz = ["equality (-4 + x^^^2 = 0)", "solveFor x","solutions L"];
 
   414 val fmz = ["equality (-4 + x^^^2 = 0)", "solveFor x","solutions L"];
 
   415 val (dI',pI',mI') = ("PolyEq.thy",["pqFormula","degree_2","polynomial","univariate","equation"],
 
   415 val (dI',pI',mI') = ("PolyEq",["pqFormula","degree_2","polynomial","univariate","equation"],
 
   416                      ["PolyEq","solve_d2_polyeq_pq_equation"]);
 
   416                      ["PolyEq","solve_d2_polyeq_pq_equation"]);
 
   417 (*val p = e_pos'; val c = []; 
   417 (*val p = e_pos'; val c = []; 
   418 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
 
   418 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
 
   419 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
 
   419 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
 
   420 
   420 
   430 	 | _ => raise error "polyeq.sml: diff.behav. in -4 + x^2 = 0 -> [x = 2, x = -2]";
 
   430 	 | _ => raise error "polyeq.sml: diff.behav. in -4 + x^2 = 0 -> [x = 2, x = -2]";
 
   431 
   431 
   432 
   432 
   433 "----- d2_pqformula10_neg ------";
 
   433 "----- d2_pqformula10_neg ------";
 
   434 val fmz = ["equality (4 + x^^^2 = 0)", "solveFor x","solutions L"];
 
   434 val fmz = ["equality (4 + x^^^2 = 0)", "solveFor x","solutions L"];
 
   435 val (dI',pI',mI') = ("PolyEq.thy",["pqFormula","degree_2","polynomial","univariate","equation"],
 
   435 val (dI',pI',mI') = ("PolyEq",["pqFormula","degree_2","polynomial","univariate","equation"],
 
   436                      ["PolyEq","solve_d2_polyeq_pq_equation"]);
 
   436                      ["PolyEq","solve_d2_polyeq_pq_equation"]);
 
   437 (*val p = e_pos'; val c = []; 
   437 (*val p = e_pos'; val c = []; 
   438 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
 
   438 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
 
   439 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
 
   439 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
 
   440 
   440 
   450 "TODO 4 + x^^^2 = 0";
 
   450 "TODO 4 + x^^^2 = 0";
 
   451 "TODO 4 + x^^^2 = 0";
 
   451 "TODO 4 + x^^^2 = 0";
 
   452 
   452 
   453 "----- d2_pqformula10 ------";
 
   453 "----- d2_pqformula10 ------";
 
   454 val fmz = ["equality (-4 + 1*x^^^2 = 0)", "solveFor x","solutions L"];
 
   454 val fmz = ["equality (-4 + 1*x^^^2 = 0)", "solveFor x","solutions L"];
 
   455 val (dI',pI',mI') = ("PolyEq.thy",["pqFormula","degree_2","polynomial","univariate","equation"],
 
   455 val (dI',pI',mI') = ("PolyEq",["pqFormula","degree_2","polynomial","univariate","equation"],
 
   456                      ["PolyEq","solve_d2_polyeq_pq_equation"]);
 
   456                      ["PolyEq","solve_d2_polyeq_pq_equation"]);
 
   457 (*val p = e_pos'; val c = []; 
   457 (*val p = e_pos'; val c = []; 
   458 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
 
   458 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
 
   459 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
 
   459 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
 
   460 
   460 
   469 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 2, x = -2]")) => ()
 
   469 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 2, x = -2]")) => ()
 
   470 	 | _ => raise error "polyeq.sml: diff.behav. in -4 + 1*x^2 = 0 -> [x = 2, x = -2]";
 
   470 	 | _ => raise error "polyeq.sml: diff.behav. in -4 + 1*x^2 = 0 -> [x = 2, x = -2]";
 
   471 
   471 
   472 "----- d2_pqformula9_neg ------";
 
   472 "----- d2_pqformula9_neg ------";
 
   473 val fmz = ["equality (4 + 1*x^^^2 = 0)", "solveFor x","solutions L"];
 
   473 val fmz = ["equality (4 + 1*x^^^2 = 0)", "solveFor x","solutions L"];
 
   474 val (dI',pI',mI') = ("PolyEq.thy",["pqFormula","degree_2","polynomial","univariate","equation"],
 
   474 val (dI',pI',mI') = ("PolyEq",["pqFormula","degree_2","polynomial","univariate","equation"],
 
   475                      ["PolyEq","solve_d2_polyeq_pq_equation"]);
 
   475                      ["PolyEq","solve_d2_polyeq_pq_equation"]);
 
   476 (*val p = e_pos'; val c = []; 
   476 (*val p = e_pos'; val c = []; 
   477 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
 
   477 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
 
   478 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
 
   478 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
 
   479 
   479 
   491 "-------------------- test thm's d2_abc_formulsxx[_neg]-----";
 
   491 "-------------------- test thm's d2_abc_formulsxx[_neg]-----";
 
   492 "-------------------- test thm's d2_abc_formulsxx[_neg]-----";
 
   492 "-------------------- test thm's d2_abc_formulsxx[_neg]-----";
 
   493 "-------------------- test thm's d2_abc_formulsxx[_neg]-----";
 
   493 "-------------------- test thm's d2_abc_formulsxx[_neg]-----";
 
   494 
   494 
   495 val fmz = ["equality (-1 +(-1)*x + 2*x^^^2 = 0)", "solveFor x","solutions L"];
 
   495 val fmz = ["equality (-1 +(-1)*x + 2*x^^^2 = 0)", "solveFor x","solutions L"];
 
   496 val (dI',pI',mI') = ("PolyEq.thy",["abcFormula","degree_2","polynomial","univariate","equation"],
 
   496 val (dI',pI',mI') = ("PolyEq",["abcFormula","degree_2","polynomial","univariate","equation"],
 
   497                      ["PolyEq","solve_d2_polyeq_abc_equation"]);
 
   497                      ["PolyEq","solve_d2_polyeq_abc_equation"]);
 
   498 (*val p = e_pos'; val c = []; 
   498 (*val p = e_pos'; val c = []; 
   499 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
 
   499 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
 
   500 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
 
   500 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
 
   501 
   501 
   509 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 c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   510 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 1, x = -1 / 2]")) => ()
 
   510 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 1, x = -1 / 2]")) => ()
 
   511 	 | _ => raise error "polyeq.sml: diff.behav. in -1 + (-1)*x + 2*x^2 = 0 -> [x = 1, x = -1/2]";
 
   511 	 | _ => raise error "polyeq.sml: diff.behav. in -1 + (-1)*x + 2*x^2 = 0 -> [x = 1, x = -1/2]";
 
   512 
   512 
   513 val fmz = ["equality ( 1 +(-1)*x + 2*x^^^2 = 0)", "solveFor x","solutions L"];
 
   513 val fmz = ["equality ( 1 +(-1)*x + 2*x^^^2 = 0)", "solveFor x","solutions L"];
 
   514 val (dI',pI',mI') = ("PolyEq.thy",["abcFormula","degree_2","polynomial","univariate","equation"],
 
   514 val (dI',pI',mI') = ("PolyEq",["abcFormula","degree_2","polynomial","univariate","equation"],
 
   515                      ["PolyEq","solve_d2_polyeq_abc_equation"]);
 
   515                      ["PolyEq","solve_d2_polyeq_abc_equation"]);
 
   516 (*val p = e_pos'; val c = []; 
   516 (*val p = e_pos'; val c = []; 
   517 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
 
   517 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
 
   518 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
 
   518 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
 
   519 
   519 
   528 "TODO 1 +(-1)*x + 2*x^^^2 = 0";
 
   528 "TODO 1 +(-1)*x + 2*x^^^2 = 0";
 
   529 "TODO 1 +(-1)*x + 2*x^^^2 = 0";
 
   529 "TODO 1 +(-1)*x + 2*x^^^2 = 0";
 
   530 
   530 
   531 (*EP-11*)
 
   531 (*EP-11*)
 
   532 val fmz = ["equality (-1 + x + 2*x^^^2 = 0)", "solveFor x","solutions L"];
 
   532 val fmz = ["equality (-1 + x + 2*x^^^2 = 0)", "solveFor x","solutions L"];
 
   533 val (dI',pI',mI') = ("PolyEq.thy",["abcFormula","degree_2","polynomial","univariate","equation"],
 
   533 val (dI',pI',mI') = ("PolyEq",["abcFormula","degree_2","polynomial","univariate","equation"],
 
   534                      ["PolyEq","solve_d2_polyeq_abc_equation"]);
 
   534                      ["PolyEq","solve_d2_polyeq_abc_equation"]);
 
   535 (*val p = e_pos'; val c = []; 
   535 (*val p = e_pos'; val c = []; 
   536 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
 
   536 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
 
   537 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
 
   537 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
 
   538 
   538 
   546 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 c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   547 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 1 / 2, x = -1]")) => ()
 
   547 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 1 / 2, x = -1]")) => ()
 
   548 	 | _ => raise error "polyeq.sml: diff.behav. in -1 + x + 2*x^2 = 0 -> [x = 1/2, x = -1]";
 
   548 	 | _ => raise error "polyeq.sml: diff.behav. in -1 + x + 2*x^2 = 0 -> [x = 1/2, x = -1]";
 
   549 
   549 
   550 val fmz = ["equality ( 1 + x + 2*x^^^2 = 0)", "solveFor x","solutions L"];
 
   550 val fmz = ["equality ( 1 + x + 2*x^^^2 = 0)", "solveFor x","solutions L"];
 
   551 val (dI',pI',mI') = ("PolyEq.thy",["abcFormula","degree_2","polynomial","univariate","equation"],
 
   551 val (dI',pI',mI') = ("PolyEq",["abcFormula","degree_2","polynomial","univariate","equation"],
 
   552                      ["PolyEq","solve_d2_polyeq_abc_equation"]);
 
   552                      ["PolyEq","solve_d2_polyeq_abc_equation"]);
 
   553 (*val p = e_pos'; val c = []; 
   553 (*val p = e_pos'; val c = []; 
   554 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
 
   554 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
 
   555 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
 
   555 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
 
   556 
   556 
   565 "TODO 1 + x + 2*x^^^2 = 0";
 
   565 "TODO 1 + x + 2*x^^^2 = 0";
 
   566 "TODO 1 + x + 2*x^^^2 = 0";
 
   566 "TODO 1 + x + 2*x^^^2 = 0";
 
   567 "TODO 1 + x + 2*x^^^2 = 0";
 
   567 "TODO 1 + x + 2*x^^^2 = 0";
 
   568 
   568 
   569 val fmz = ["equality (-2 + 1*x + x^^^2 = 0)", "solveFor x","solutions L"];
 
   569 val fmz = ["equality (-2 + 1*x + x^^^2 = 0)", "solveFor x","solutions L"];
 
   570 val (dI',pI',mI') = ("PolyEq.thy",["abcFormula","degree_2","polynomial","univariate","equation"],
 
   570 val (dI',pI',mI') = ("PolyEq",["abcFormula","degree_2","polynomial","univariate","equation"],
 
   571                      ["PolyEq","solve_d2_polyeq_abc_equation"]);
 
   571                      ["PolyEq","solve_d2_polyeq_abc_equation"]);
 
   572 (*val p = e_pos'; val c = []; 
   572 (*val p = e_pos'; val c = []; 
   573 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
 
   573 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
 
   574 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
 
   574 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
 
   575 
   575 
   583 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 c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   584 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 1, x = -2]")) => ()
 
   584 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 1, x = -2]")) => ()
 
   585 	 | _ => raise error "polyeq.sml: diff.behav. in -2 + 1*x + x^2 = 0 -> [x = 1, x = -2]";
 
   585 	 | _ => raise error "polyeq.sml: diff.behav. in -2 + 1*x + x^2 = 0 -> [x = 1, x = -2]";
 
   586 
   586 
   587 val fmz = ["equality ( 2 + 1*x + x^^^2 = 0)", "solveFor x","solutions L"];
 
   587 val fmz = ["equality ( 2 + 1*x + x^^^2 = 0)", "solveFor x","solutions L"];
 
   588 val (dI',pI',mI') = ("PolyEq.thy",["abcFormula","degree_2","polynomial","univariate","equation"],
 
   588 val (dI',pI',mI') = ("PolyEq",["abcFormula","degree_2","polynomial","univariate","equation"],
 
   589                      ["PolyEq","solve_d2_polyeq_abc_equation"]);
 
   589                      ["PolyEq","solve_d2_polyeq_abc_equation"]);
 
   590 (*val p = e_pos'; val c = []; 
   590 (*val p = e_pos'; val c = []; 
   591 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
 
   591 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
 
   592 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
 
   592 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
 
   593 
   593 
   603 "TODO 2 + 1*x + x^^^2 = 0";
 
   603 "TODO 2 + 1*x + x^^^2 = 0";
 
   604 "TODO 2 + 1*x + x^^^2 = 0";
 
   604 "TODO 2 + 1*x + x^^^2 = 0";
 
   605 
   605 
   606 (*EP-12*)
 
   606 (*EP-12*)
 
   607 val fmz = ["equality (-2 + x + x^^^2 = 0)", "solveFor x","solutions L"];
 
   607 val fmz = ["equality (-2 + x + x^^^2 = 0)", "solveFor x","solutions L"];
 
   608 val (dI',pI',mI') = ("PolyEq.thy",["abcFormula","degree_2","polynomial","univariate","equation"],
 
   608 val (dI',pI',mI') = ("PolyEq",["abcFormula","degree_2","polynomial","univariate","equation"],
 
   609                      ["PolyEq","solve_d2_polyeq_abc_equation"]);
 
   609                      ["PolyEq","solve_d2_polyeq_abc_equation"]);
 
   610 (*val p = e_pos'; val c = []; 
   610 (*val p = e_pos'; val c = []; 
   611 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
 
   611 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
 
   612 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
 
   612 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
 
   613 
   613 
   621 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 c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   622 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 1, x = -2]")) => ()
 
   622 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 1, x = -2]")) => ()
 
   623 	 | _ => raise error "polyeq.sml: diff.behav. in -2 + x + x^2 = 0 -> [x = 1, x = -2]";
 
   623 	 | _ => raise error "polyeq.sml: diff.behav. in -2 + x + x^2 = 0 -> [x = 1, x = -2]";
 
   624 
   624 
   625 val fmz = ["equality ( 2 + x + x^^^2 = 0)", "solveFor x","solutions L"];
 
   625 val fmz = ["equality ( 2 + x + x^^^2 = 0)", "solveFor x","solutions L"];
 
   626 val (dI',pI',mI') = ("PolyEq.thy",["abcFormula","degree_2","polynomial","univariate","equation"],
 
   626 val (dI',pI',mI') = ("PolyEq",["abcFormula","degree_2","polynomial","univariate","equation"],
 
   627                      ["PolyEq","solve_d2_polyeq_abc_equation"]);
 
   627                      ["PolyEq","solve_d2_polyeq_abc_equation"]);
 
   628 (*val p = e_pos'; val c = []; 
   628 (*val p = e_pos'; val c = []; 
   629 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
 
   629 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
 
   630 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
 
   630 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
 
   631 
   631 
   641 "TODO 2 + x + x^^^2 = 0";
 
   641 "TODO 2 + x + x^^^2 = 0";
 
   642 "TODO 2 + x + x^^^2 = 0";
 
   642 "TODO 2 + x + x^^^2 = 0";
 
   643 
   643 
   644 (*EP-13*)
 
   644 (*EP-13*)
 
   645 val fmz = ["equality (-8 + 2*x^^^2 = 0)", "solveFor x","solutions L"];
 
   645 val fmz = ["equality (-8 + 2*x^^^2 = 0)", "solveFor x","solutions L"];
 
   646 val (dI',pI',mI') = ("PolyEq.thy",["abcFormula","degree_2","polynomial","univariate","equation"],
 
   646 val (dI',pI',mI') = ("PolyEq",["abcFormula","degree_2","polynomial","univariate","equation"],
 
   647                      ["PolyEq","solve_d2_polyeq_abc_equation"]);
 
   647                      ["PolyEq","solve_d2_polyeq_abc_equation"]);
 
   648 (*val p = e_pos'; val c = []; 
   648 (*val p = e_pos'; val c = []; 
   649 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
 
   649 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
 
   650 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
 
   650 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
 
   651 
   651 
   659 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 c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   660 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 2, x = -2]")) => ()
 
   660 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 2, x = -2]")) => ()
 
   661 	 | _ => raise error "polyeq.sml: diff.behav. in -8 + 2*x^2 = 0 -> [x = 2, x = -2]";
 
   661 	 | _ => raise error "polyeq.sml: diff.behav. in -8 + 2*x^2 = 0 -> [x = 2, x = -2]";
 
   662 
   662 
   663 val fmz = ["equality ( 8+ 2*x^^^2 = 0)", "solveFor x","solutions L"];
 
   663 val fmz = ["equality ( 8+ 2*x^^^2 = 0)", "solveFor x","solutions L"];
 
   664 val (dI',pI',mI') = ("PolyEq.thy",["abcFormula","degree_2","polynomial","univariate","equation"],
 
   664 val (dI',pI',mI') = ("PolyEq",["abcFormula","degree_2","polynomial","univariate","equation"],
 
   665                      ["PolyEq","solve_d2_polyeq_abc_equation"]);
 
   665                      ["PolyEq","solve_d2_polyeq_abc_equation"]);
 
   666 (*val p = e_pos'; val c = []; 
   666 (*val p = e_pos'; val c = []; 
   667 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
 
   667 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
 
   668 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
 
   668 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
 
   669 
   669 
   678 "TODO 8+ 2*x^^^2 = 0";
 
   678 "TODO 8+ 2*x^^^2 = 0";
 
   679 "TODO 8+ 2*x^^^2 = 0";
 
   679 "TODO 8+ 2*x^^^2 = 0";
 
   680 
   680 
   681 (*EP-14*)
 
   681 (*EP-14*)
 
   682 val fmz = ["equality (-4 + x^^^2 = 0)", "solveFor x","solutions L"];
 
   682 val fmz = ["equality (-4 + x^^^2 = 0)", "solveFor x","solutions L"];
 
   683 val (dI',pI',mI') = ("PolyEq.thy",["abcFormula","degree_2","polynomial","univariate","equation"], ["PolyEq","solve_d2_polyeq_abc_equation"]);
 
   683 val (dI',pI',mI') = ("PolyEq",["abcFormula","degree_2","polynomial","univariate","equation"], ["PolyEq","solve_d2_polyeq_abc_equation"]);
 
   684 (*val p = e_pos'; val c = []; 
   684 (*val p = e_pos'; val c = []; 
   685 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
 
   685 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
 
   686 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
 
   686 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
 
   687 
   687 
   688 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
 
   688 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
 
   696 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 2, x = -2]")) => ()
 
   696 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 2, x = -2]")) => ()
 
   697 	 | _ => raise error "polyeq.sml: diff.behav. in -4 + x^2 = 0 -> [x = 2, x = -2]";
 
   697 	 | _ => raise error "polyeq.sml: diff.behav. in -4 + x^2 = 0 -> [x = 2, x = -2]";
 
   698 
   698 
   699 
   699 
   700 val fmz = ["equality ( 4+ x^^^2 = 0)", "solveFor x","solutions L"];
 
   700 val fmz = ["equality ( 4+ x^^^2 = 0)", "solveFor x","solutions L"];
 
   701 val (dI',pI',mI') = ("PolyEq.thy",["abcFormula","degree_2","polynomial","univariate","equation"], ["PolyEq","solve_d2_polyeq_abc_equation"]);
 
   701 val (dI',pI',mI') = ("PolyEq",["abcFormula","degree_2","polynomial","univariate","equation"], ["PolyEq","solve_d2_polyeq_abc_equation"]);
 
   702 (*val p = e_pos'; val c = []; 
   702 (*val p = e_pos'; val c = []; 
   703 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
 
   703 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
 
   704 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
 
   704 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
 
   705 
   705 
   706 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
 
   706 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
 
   714 "TODO 4+ x^^^2 = 0";
 
   714 "TODO 4+ x^^^2 = 0";
 
   715 "TODO 4+ x^^^2 = 0";
 
   715 "TODO 4+ x^^^2 = 0";
 
   716 
   716 
   717 (*EP-15*)
 
   717 (*EP-15*)
 
   718 val fmz = ["equality (2*x + 2*x^^^2 = 0)", "solveFor x","solutions L"];
 
   718 val fmz = ["equality (2*x + 2*x^^^2 = 0)", "solveFor x","solutions L"];
 
   719 val (dI',pI',mI') = ("PolyEq.thy",["abcFormula","degree_2","polynomial","univariate","equation"],
 
   719 val (dI',pI',mI') = ("PolyEq",["abcFormula","degree_2","polynomial","univariate","equation"],
 
   720                      ["PolyEq","solve_d2_polyeq_abc_equation"]);
 
   720                      ["PolyEq","solve_d2_polyeq_abc_equation"]);
 
   721 (*val p = e_pos'; val c = []; 
   721 (*val p = e_pos'; val c = []; 
   722 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
 
   722 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
 
   723 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
 
   723 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
 
   724 
   724 
   732 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 c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   733 case f of Form' (FormKF (~1,EdUndef,_,Nundef,"[x = 0, x = -1]")) => ()
 
   733 case f of Form' (FormKF (~1,EdUndef,_,Nundef,"[x = 0, x = -1]")) => ()
 
   734 	 | _ => raise error "polyeq.sml: diff.behav. in x + x^2 = 0 -> [x = 0, x = -1]";
 
   734 	 | _ => raise error "polyeq.sml: diff.behav. in x + x^2 = 0 -> [x = 0, x = -1]";
 
   735 
   735 
   736 val fmz = ["equality (1*x + x^^^2 = 0)", "solveFor x","solutions L"];
 
   736 val fmz = ["equality (1*x + x^^^2 = 0)", "solveFor x","solutions L"];
 
   737 val (dI',pI',mI') = ("PolyEq.thy",["abcFormula","degree_2","polynomial","univariate","equation"],
 
   737 val (dI',pI',mI') = ("PolyEq",["abcFormula","degree_2","polynomial","univariate","equation"],
 
   738                      ["PolyEq","solve_d2_polyeq_abc_equation"]);
 
   738                      ["PolyEq","solve_d2_polyeq_abc_equation"]);
 
   739 (*val p = e_pos'; val c = []; 
   739 (*val p = e_pos'; val c = []; 
   740 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
 
   740 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
 
   741 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
 
   741 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
 
   742 
   742 
   751 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 0, x = -1]")) => ()
 
   751 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 0, x = -1]")) => ()
 
   752 	 | _ => raise error "polyeq.sml: diff.behav. in x + x^2 = 0 -> [x = 0, x = -1]";
 
   752 	 | _ => raise error "polyeq.sml: diff.behav. in x + x^2 = 0 -> [x = 0, x = -1]";
 
   753 
   753 
   754 (*EP-16*)
 
   754 (*EP-16*)
 
   755 val fmz = ["equality (x + 2*x^^^2 = 0)", "solveFor x","solutions L"];
 
   755 val fmz = ["equality (x + 2*x^^^2 = 0)", "solveFor x","solutions L"];
 
   756 val (dI',pI',mI') = ("PolyEq.thy",["abcFormula","degree_2","polynomial","univariate","equation"],
 
   756 val (dI',pI',mI') = ("PolyEq",["abcFormula","degree_2","polynomial","univariate","equation"],
 
   757                      ["PolyEq","solve_d2_polyeq_abc_equation"]);
 
   757                      ["PolyEq","solve_d2_polyeq_abc_equation"]);
 
   758 (*val p = e_pos'; val c = []; 
   758 (*val p = e_pos'; val c = []; 
   759 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
 
   759 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
 
   760 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
 
   760 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
 
   761 
   761 
   770 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 0, x = -1 / 2]")) => ()
 
   770 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 0, x = -1 / 2]")) => ()
 
   771 	 | _ => raise error "polyeq.sml: diff.behav. in x + x^2 = 0 -> [x = 0, x = -1 / 2]";
 
   771 	 | _ => raise error "polyeq.sml: diff.behav. in x + x^2 = 0 -> [x = 0, x = -1 / 2]";
 
   772 
   772 
   773 (*EP-//*)
 
   773 (*EP-//*)
 
   774 val fmz = ["equality (x + x^^^2 = 0)", "solveFor x","solutions L"];
 
   774 val fmz = ["equality (x + x^^^2 = 0)", "solveFor x","solutions L"];
 
   775 val (dI',pI',mI') = ("PolyEq.thy",["abcFormula","degree_2","polynomial","univariate","equation"],
 
   775 val (dI',pI',mI') = ("PolyEq",["abcFormula","degree_2","polynomial","univariate","equation"],
 
   776                      ["PolyEq","solve_d2_polyeq_abc_equation"]);
 
   776                      ["PolyEq","solve_d2_polyeq_abc_equation"]);
 
   777 (*val p = e_pos'; val c = []; 
   777 (*val p = e_pos'; val c = []; 
   778 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
 
   778 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
 
   779 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
 
   779 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
 
   780 
   780 
   793 "----------- (-8 - 2*x + x^^^2 = 0),  (*Schalk 2, S.67 Nr.31.b----";
 
   793 "----------- (-8 - 2*x + x^^^2 = 0),  (*Schalk 2, S.67 Nr.31.b----";
 
   794 "----------- (-8 - 2*x + x^^^2 = 0),  (*Schalk 2, S.67 Nr.31.b----";
 
   794 "----------- (-8 - 2*x + x^^^2 = 0),  (*Schalk 2, S.67 Nr.31.b----";
 
   795  val fmz = ["equality (-8 - 2*x + x^^^2 = 0)", (*Schalk 2, S.67 Nr.31.b*)
 
   795  val fmz = ["equality (-8 - 2*x + x^^^2 = 0)", (*Schalk 2, S.67 Nr.31.b*)
 
   796  	    "solveFor x","solutions L"];
 
   796  	    "solveFor x","solutions L"];
 
   797  val (dI',pI',mI') =
 
   797  val (dI',pI',mI') =
 
   798      ("PolyEq.thy",["degree_2","expanded","univariate","equation"],
 
   798      ("PolyEq",["degree_2","expanded","univariate","equation"],
 
   799       ["PolyEq","complete_square"]);
 
   799       ["PolyEq","complete_square"]);
 
   800 (* val p = e_pos'; val c = []; 
   800 (* val p = e_pos'; val c = []; 
   801  val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
 
   801  val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
 
   802  val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
 
   802  val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
 
   803 
   803 
   804 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
 
   804 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
 
   805 val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   805 val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   806  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 c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   807  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 c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   808  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 c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   809  (*Apply_Method ("PolyEq.thy","complete_square")*)
 
   809  (*Apply_Method ("PolyEq","complete_square")*)
 
   810  val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   810  val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   811  (*"-8 - 2 * x + x ^^^ 2 = 0", nxt = Rewrite_Set_Inst ... "complete_square*)
 
   811  (*"-8 - 2 * x + x ^^^ 2 = 0", nxt = Rewrite_Set_Inst ... "complete_square*)
 
   812  val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   812  val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   813  (*"-8 + (2 / 2 - x) ^^^ 2 = (2 / 2) ^^^ 2", nxt = Rewrite("square_explicit1"*)
 
   813  (*"-8 + (2 / 2 - x) ^^^ 2 = (2 / 2) ^^^ 2", nxt = Rewrite("square_explicit1"*)
 
   814  val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   814  val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   852  else raise error "polyeq.sml: diff.behav. in 'rewrite_set_.. PolyEq_erls";*)
 
   852  else raise error "polyeq.sml: diff.behav. in 'rewrite_set_.. PolyEq_erls";*)
 
   853 (* *)
 
   853 (* *)
 
   854  val fmz = ["equality (3 - 10*x + 3*x^^^2 = 0)",
 
   854  val fmz = ["equality (3 - 10*x + 3*x^^^2 = 0)",
 
   855  	    "solveFor x","solutions L"];
 
   855  	    "solveFor x","solutions L"];
 
   856  val (dI',pI',mI') =
 
   856  val (dI',pI',mI') =
 
   857      ("PolyEq.thy",["degree_2","expanded","univariate","equation"],
 
   857      ("PolyEq",["degree_2","expanded","univariate","equation"],
 
   858       ["PolyEq","complete_square"]);
 
   858       ["PolyEq","complete_square"]);
 
   859 (* val p = e_pos'; val c = []; 
   859 (* val p = e_pos'; val c = []; 
   860  val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
 
   860  val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
 
   861  val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
 
   861  val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
 
   862 
   862 
   866  val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   866  val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   867  val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   867  val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   868  val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   868  val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   869  val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   869  val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   870  val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   870  val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   871  (*Apply_Method ("PolyEq.thy","complete_square")*)
 
   871  (*Apply_Method ("PolyEq","complete_square")*)
 
   872  val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
 
   872  val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
 
   873 
   873 
   874 "----------- (-16 + 4*x + 2*x^^^2 = 0), --------------------------";
 
   874 "----------- (-16 + 4*x + 2*x^^^2 = 0), --------------------------";
 
   875 "----------- (-16 + 4*x + 2*x^^^2 = 0), --------------------------";
 
   875 "----------- (-16 + 4*x + 2*x^^^2 = 0), --------------------------";
 
   876 "----------- (-16 + 4*x + 2*x^^^2 = 0), --------------------------";
 
   876 "----------- (-16 + 4*x + 2*x^^^2 = 0), --------------------------";
 
   877  val fmz = ["equality (-16 + 4*x + 2*x^^^2 = 0)",
 
   877  val fmz = ["equality (-16 + 4*x + 2*x^^^2 = 0)",
 
   878  	    "solveFor x","solutions L"];
 
   878  	    "solveFor x","solutions L"];
 
   879  val (dI',pI',mI') =
 
   879  val (dI',pI',mI') =
 
   880      ("PolyEq.thy",["degree_2","expanded","univariate","equation"],
 
   880      ("PolyEq",["degree_2","expanded","univariate","equation"],
 
   881       ["PolyEq","complete_square"]);
 
   881       ["PolyEq","complete_square"]);
 
   882 (* val p = e_pos'; val c = []; 
   882 (* val p = e_pos'; val c = []; 
   883  val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
 
   883  val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
 
   884  val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*) 
   884  val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*) 
   885 
   885 
   889  val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   889  val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   890  val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   890  val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   891  val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   891  val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   892  val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   892  val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   893  val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   893  val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   894  (*Apply_Method ("PolyEq.thy","complete_square")*)
 
   894  (*Apply_Method ("PolyEq","complete_square")*)
 
   895  val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   895  val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   896  val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   896  val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   897  val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   897  val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   898  val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   898  val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   899  val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   899  val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   911 "----------- (a*b - (a+b)*x + x^^^2 = 0), (*Schalk 2,S.68Nr.44.a*)";
 
   911 "----------- (a*b - (a+b)*x + x^^^2 = 0), (*Schalk 2,S.68Nr.44.a*)";
 
   912 "----------- (a*b - (a+b)*x + x^^^2 = 0), (*Schalk 2,S.68Nr.44.a*)";
 
   912 "----------- (a*b - (a+b)*x + x^^^2 = 0), (*Schalk 2,S.68Nr.44.a*)";
 
   913  val fmz = ["equality (a*b - (a+b)*x + x^^^2 = 0)",
 
   913  val fmz = ["equality (a*b - (a+b)*x + x^^^2 = 0)",
 
   914  	    "solveFor x","solutions L"];
 
   914  	    "solveFor x","solutions L"];
 
   915  val (dI',pI',mI') =
 
   915  val (dI',pI',mI') =
 
   916      ("PolyEq.thy",["degree_2","expanded","univariate","equation"],
 
   916      ("PolyEq",["degree_2","expanded","univariate","equation"],
 
   917       ["PolyEq","complete_square"]);
 
   917       ["PolyEq","complete_square"]);
 
   918 (* val p = e_pos'; val c = []; 
   918 (* val p = e_pos'; val c = []; 
   919  val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
 
   919  val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
 
   920  val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
 
   920  val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
 
   921 
   921 
   954 "----------- (-64 + x^^^2 = 0), (*Schalk 2, S.66 Nr.1.a~--------*)";
 
   954 "----------- (-64 + x^^^2 = 0), (*Schalk 2, S.66 Nr.1.a~--------*)";
 
   955 "----------- (-64 + x^^^2 = 0), (*Schalk 2, S.66 Nr.1.a~--------*)";
 
   955 "----------- (-64 + x^^^2 = 0), (*Schalk 2, S.66 Nr.1.a~--------*)";
 
   956  val fmz = ["equality (-64 + x^^^2 = 0)",(*Schalk 2, S.66 Nr.1.a~*)
 
   956  val fmz = ["equality (-64 + x^^^2 = 0)",(*Schalk 2, S.66 Nr.1.a~*)
 
   957  	    "solveFor x","solutions L"];
 
   957  	    "solveFor x","solutions L"];
 
   958  val (dI',pI',mI') =
 
   958  val (dI',pI',mI') =
 
   959      ("PolyEq.thy",["degree_2","expanded","univariate","equation"],
 
   959      ("PolyEq",["degree_2","expanded","univariate","equation"],
 
   960       ["PolyEq","complete_square"]);
 
   960       ["PolyEq","complete_square"]);
 
   961 (* val p = e_pos'; val c = []; 
   961 (* val p = e_pos'; val c = []; 
   962  val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
 
   962  val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
 
   963  val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
 
   963  val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
 
   964 
   964 
   985 "----------- (-147 + 3*x^^^2 = 0), (*Schalk 2, S.66 Nr.1.b------*)";
 
   985 "----------- (-147 + 3*x^^^2 = 0), (*Schalk 2, S.66 Nr.1.b------*)";
 
   986 "----------- (-147 + 3*x^^^2 = 0), (*Schalk 2, S.66 Nr.1.b------*)";
 
   986 "----------- (-147 + 3*x^^^2 = 0), (*Schalk 2, S.66 Nr.1.b------*)";
 
   987  val fmz = ["equality (-147 + 3*x^^^2 = 0)",(*Schalk 2, S.66 Nr.1.b*)
 
   987  val fmz = ["equality (-147 + 3*x^^^2 = 0)",(*Schalk 2, S.66 Nr.1.b*)
 
   988  	    "solveFor x","solutions L"];
 
   988  	    "solveFor x","solutions L"];
 
   989  val (dI',pI',mI') =
 
   989  val (dI',pI',mI') =
 
   990      ("PolyEq.thy",["degree_2","expanded","univariate","equation"],
 
   990      ("PolyEq",["degree_2","expanded","univariate","equation"],
 
   991       ["PolyEq","complete_square"]);
 
   991       ["PolyEq","complete_square"]);
 
   992 (* val p = e_pos'; val c = []; 
   992 (* val p = e_pos'; val c = []; 
   993  val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
 
   993  val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
 
   994  val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
 
   994  val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
 
   995 
   995 
  1015 "----------- (3*x - 1 - (5*x - (2 - 4*x)) = -11),(*Schalk Is86Bsp5";
 
  1015 "----------- (3*x - 1 - (5*x - (2 - 4*x)) = -11),(*Schalk Is86Bsp5";
 
  1016 (*EP-17 Schalk_I_p86_n5*)
 
  1016 (*EP-17 Schalk_I_p86_n5*)
 
  1017 val fmz = ["equality (3*x - 1 - (5*x - (2 - 4*x)) = -11)","solveFor x","solutions L"];
 
  1017 val fmz = ["equality (3*x - 1 - (5*x - (2 - 4*x)) = -11)","solveFor x","solutions L"];
 
  1018 (* refine fmz ["univariate","equation"];
 
  1018 (* refine fmz ["univariate","equation"];
 
  1019 *)
 
  1019 *)
 
  1020 val (dI',pI',mI') = ("PolyEq.thy",["univariate","equation"],["no_met"]);
 
  1020 val (dI',pI',mI') = ("PolyEq",["univariate","equation"],["no_met"]);
 
  1021 (*val p = e_pos'; 
  1021 (*val p = e_pos'; 
  1022 val c = []; 
  1022 val c = []; 
  1023 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
 
  1023 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
 
  1024 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
 
  1024 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
 
  1025 
  1025 
  1034 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 
  1034 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 
  1035 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 
  1035 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 
  1036 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 
  1036 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 
  1037 (* val nxt =
 
  1037 (* val nxt =
 
  1038   ("Subproblem",
 
  1038   ("Subproblem",
 
  1039    Subproblem ("PolyEq.thy",["polynomial","univariate","equation"]))
 
  1039    Subproblem ("PolyEq",["polynomial","univariate","equation"]))
 
  1040   : string * tac *)
 
  1040   : string * tac *)
 
  1041 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 
  1041 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 
  1042 (*val nxt =
 
  1042 (*val nxt =
 
  1043   ("Model_Problem",
 
  1043   ("Model_Problem",
 
  1044    Model_Problem ["degree_1","polynomial","univariate","equation"])
 
  1044    Model_Problem ["degree_1","polynomial","univariate","equation"])
 
  1059 "----------- ((x+1)*(x+2) - (3*x - 2)^^^2=.. Schalk II s.68 Bsp 37";
 
  1059 "----------- ((x+1)*(x+2) - (3*x - 2)^^^2=.. Schalk II s.68 Bsp 37";
 
  1060 "----------- ((x+1)*(x+2) - (3*x - 2)^^^2=.. Schalk II s.68 Bsp 37";
 
  1060 "----------- ((x+1)*(x+2) - (3*x - 2)^^^2=.. Schalk II s.68 Bsp 37";
 
  1061 (*is in rlang.sml, too*)
 
  1061 (*is in rlang.sml, too*)
 
  1062 val fmz = ["equality ((x+1)*(x+2) - (3*x - 2)^^^2=(2*x - 1)^^^2+(3*x - 1)*(x+1))",
 
  1062 val fmz = ["equality ((x+1)*(x+2) - (3*x - 2)^^^2=(2*x - 1)^^^2+(3*x - 1)*(x+1))",
 
  1063 	   "solveFor x","solutions L"];
 
  1063 	   "solveFor x","solutions L"];
 
  1064 val (dI',pI',mI') = ("PolyEq.thy",["univariate","equation"],["no_met"]);
 
  1064 val (dI',pI',mI') = ("PolyEq",["univariate","equation"],["no_met"]);
 
  1065 
  1065 
  1066 (*val p = e_pos'; val c = []; 
  1066 (*val p = e_pos'; val c = []; 
  1067 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
 
  1067 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
 
  1068 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
 
  1068 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
 
  1069 
  1069 
  1080 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 
  1080 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 
  1081 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 
  1081 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 
  1082 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 
  1082 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 
  1083 (* val nxt =
 
  1083 (* val nxt =
 
  1084   ("Subproblem",
 
  1084   ("Subproblem",
 
  1085    Subproblem ("PolyEq.thy",["polynomial","univariate","equation"]))
 
  1085    Subproblem ("PolyEq",["polynomial","univariate","equation"]))
 
  1086   : string * tac*)
 
  1086   : string * tac*)
 
  1087 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 
  1087 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 
  1088 (*val nxt =
 
  1088 (*val nxt =
 
  1089   ("Model_Problem",
 
  1089   ("Model_Problem",
 
  1090    Model_Problem ["abcFormula","degree_2","polynomial","univariate","equation"])
 
  1090    Model_Problem ["abcFormula","degree_2","polynomial","univariate","equation"])
 
  1104 "    -4 + x^^^2 =0     ";
 
  1104 "    -4 + x^^^2 =0     ";
 
  1105 "    -4 + x^^^2 =0     ";
 
  1105 "    -4 + x^^^2 =0     ";
 
  1106 val fmz = ["equality ( -4 + x^^^2 =0)", "solveFor x","solutions L"];
 
  1106 val fmz = ["equality ( -4 + x^^^2 =0)", "solveFor x","solutions L"];
 
  1107 (* val fmz = ["equality (1 + x^^^2 =0)", "solveFor x","solutions L"];*)
 
  1107 (* val fmz = ["equality (1 + x^^^2 =0)", "solveFor x","solutions L"];*)
 
  1108 (*val fmz = ["equality (0 =0)", "solveFor x","solutions L"];*)
 
  1108 (*val fmz = ["equality (0 =0)", "solveFor x","solutions L"];*)
 
  1109 val (dI',pI',mI') = ("PolyEq.thy",["univariate","equation"],["no_met"]);
 
  1109 val (dI',pI',mI') = ("PolyEq",["univariate","equation"],["no_met"]);
 
  1110 (*val p = e_pos'; 
  1110 (*val p = e_pos'; 
  1111 val c = []; 
  1111 val c = []; 
  1112 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
 
  1112 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
 
  1113 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
 
  1113 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
 
  1114 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
 
  1114 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
 
  1167 "----------- interSteps ([1],Res); on Schalk Is86Bsp5-------------";
 
  1167 "----------- interSteps ([1],Res); on Schalk Is86Bsp5-------------";
 
  1168 "----------- interSteps ([1],Res); on Schalk Is86Bsp5-------------";
 
  1168 "----------- interSteps ([1],Res); on Schalk Is86Bsp5-------------";
 
  1169 states:=[];
 
  1169 states:=[];
 
  1170 CalcTree
 
  1170 CalcTree
 
  1171 [(["equality (3*x - 1 - (5*x - (2 - 4*x)) = -11)","solveFor x","solutions L"], 
  1171 [(["equality (3*x - 1 - (5*x - (2 - 4*x)) = -11)","solveFor x","solutions L"], 
  1172   ("PolyEq.thy",["univariate","equation"],["no_met"]))];
 
  1172   ("PolyEq",["univariate","equation"],["no_met"]))];
 
  1173 Iterator 1;
 
  1173 Iterator 1;
 
  1174 moveActiveRoot 1;
 
  1174 moveActiveRoot 1;
 
  1175 autoCalculate 1 CompleteCalc;
 
  1175 autoCalculate 1 CompleteCalc;
 
  1176 val ((pt,p),_) = get_calc 1; show_pt pt;
 
  1176 val ((pt,p),_) = get_calc 1; show_pt pt;
 
  1177 
  1177
wneuper/isa