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/rooteq.sml
changeset 60331 40eb8aa2b0d6
parent 60309 70a1d102660d
parent 60329 0c10aeff57d7
child 60558 2350ba2640fd
equal deleted inserted replaced
60316:63cecf440235 60331:40eb8aa2b0d6 
   116 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 
   116 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 
   117 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 
   117 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 
   118 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 
   118 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 
   119 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 
   119 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 
   120 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 
   120 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 
   121 if f = Form' (Test_Out.FormKF (~1, EdUndef, 0, Nundef, "1 + -25 * x = 0")) then ()
 
   121 if f = Form' (Test_Out.FormKF (~1, EdUndef, 0, Nundef, "1 + - 25 * x = 0")) then ()
 
   122 else error "rooteq.sml: diff.behav.poly in (1/sqrt(x)=5)";
 
   122 else error "rooteq.sml: diff.behav.poly in (1/sqrt(x)=5)";
 
   123 (*-> Subproblem ("PolyEq", ["polynomial", ...])*)
 
   123 (*-> Subproblem ("PolyEq", ["polynomial", ...])*)
 
   124 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 
   124 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 
   125 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 
   125 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 
   126 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 
   126 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 
   158 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 
   158 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 
   159 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 
   159 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 
   160 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 
   160 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 
   161 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 
   161 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 
   162 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 
   162 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 
   163 if f = Form' (Test_Out.FormKF (~1, EdUndef, 0, Nundef, "-24 + x = 0")) then ()
 
   163 if f = Form' (Test_Out.FormKF (~1, EdUndef, 0, Nundef, "- 24 + x = 0")) then ()
 
   164 else error "rooteq.sml: diff.behav.poly in sqrt(x+1)=5";
 
   164 else error "rooteq.sml: diff.behav.poly in sqrt(x+1)=5";
 
   165 (*-> Subproblem ("PolyEq", ["polynomial", ...])*)
 
   165 (*-> Subproblem ("PolyEq", ["polynomial", ...])*)
 
   166 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 
   166 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 
   167 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 
   167 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 
   168 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 
   168 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 
   189 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 
   189 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 
   190 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 
   190 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 
   191 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 
   191 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 
   192 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 
   192 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 
   193 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 
   193 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 
   194 if f = Form' (Test_Out.FormKF (~1, EdUndef, 0, Nundef, "-184 + 46 * x = 0")) then ()
 
   194 if f = Form' (Test_Out.FormKF (~1, EdUndef, 0, Nundef, "- 184 + 46 * x = 0")) then ()
 
   195 else error "rooteq.sml: diff.behav.poly in 4*sqrt(4*x+2)=3*sqrt(2*x+24)";
 
   195 else error "rooteq.sml: diff.behav.poly in 4*sqrt(4*x+2)=3*sqrt(2*x+24)";
 
   196 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 
   196 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 
   197 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 
   197 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 
   198 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 
   198 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 
   199 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 
   199 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 
   220 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   220 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   221 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   221 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   222 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   222 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   223 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   223 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   224 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   224 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   225 (*"13 + 13 * x + -2 * sqrt ((4 + 4 * x) * (9 + 9 * x)) = 1 + x"))
 
   225 (*"13 + 13 * x + - 2 * sqrt ((4 + 4 * x) * (9 + 9 * x)) = 1 + x"))
 
   226 val nxt = ("Subproblem",Subproblem ("RootEq",["univariate", "equation"]))*)
 
   226 val nxt = ("Subproblem",Subproblem ("RootEq",["univariate", "equation"]))*)
 
   227 val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   227 val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   228 (*val nxt = Model_Problem ["sq", "rootX", "univariate", "equation"]) *)
 
   228 (*val nxt = Model_Problem ["sq", "rootX", "univariate", "equation"]) *)
 
   229 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   229 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   230 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   230 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   260 
   260 
   261 
   261 
   262 
   262 
   263 "--------------(sqrt(x+1)+sqrt(4*x+4)=sqrt(9*x+9))---------- SUBPBL.2.------";
 
   263 "--------------(sqrt(x+1)+sqrt(4*x+4)=sqrt(9*x+9))---------- SUBPBL.2.------";
 
   264 val fmz = 
   264 val fmz = 
   265     ["equality (13 + 13 * x + -2 * sqrt ((4 + 4 * x) * (9 + 9 * x)) = 1 + x)",
 
   265     ["equality (13 + 13 * x + - 2 * sqrt ((4 + 4 * x) * (9 + 9 * x)) = 1 + x)",
 
   266      "solveFor x", "solutions L"];
 
   266      "solveFor x", "solutions L"];
 
   267 val (dI',pI',mI') = ("RootEq",["sq", "rootX", "univariate", "equation"],
 
   267 val (dI',pI',mI') = ("RootEq",["sq", "rootX", "univariate", "equation"],
 
   268 		     ["RootEq", "solve_sq_root_equation"]);
 
   268 		     ["RootEq", "solve_sq_root_equation"]);
 
   269 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
 
   269 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
 
   270 val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   270 val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   330 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 c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   331 val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   331 val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   332 (*val nxt = ("Specify_Method",Specify_Method ["PolyEq", "normalise_poly"])*)
 
   332 (*val nxt = ("Specify_Method",Specify_Method ["PolyEq", "normalise_poly"])*)
 
   333 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   333 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   334 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   334 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   335 (*val p = ([3,2],Res)val f = Form' (Test_Out.FormKF (~1,EdUndef,2,Nundef,"-1 + x = 0"))
 
   335 (*val p = ([3,2],Res)val f = Form' (Test_Out.FormKF (~1,EdUndef,2,Nundef,"- 1 + x = 0"))
 
   336 val nxt = Subproblem ("PolyEq",["polynomial", "univariate", "equation"]))*)
 
   336 val nxt = Subproblem ("PolyEq",["polynomial", "univariate", "equation"]))*)
 
   337 if f = Form' (Test_Out.FormKF (~1, EdUndef, 0, Nundef, "-1 + x = 0")) then ()
 
   337 if f = Form' (Test_Out.FormKF (~1, EdUndef, 0, Nundef, "- 1 + x = 0")) then ()
 
   338 else error "rooteq.sml: diff.behav.poly in sqrt(x+1)+sqrt(4*x+4)=sqrt..";
 
   338 else error "rooteq.sml: diff.behav.poly in sqrt(x+1)+sqrt(4*x+4)=sqrt..";
 
   339 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   339 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   340 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   340 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   341 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   341 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   342 val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   342 val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   458 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   458 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   459 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   459 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   460 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   460 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   461 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   461 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   462 val (p,_,f,nxt,_,pt) = me nxt p c pt;                                  
   462 val (p,_,f,nxt,_,pt) = me nxt p c pt;                                  
   463 case f of Form' (Test_Out.FormKF (~1,EdUndef,0,Nundef,"[x = -2]")) => ()
 
   463 case f of Form' (Test_Out.FormKF (~1,EdUndef,0,Nundef,"[x = - 2]")) => ()
 
   464 	 | _ => error "rooteq.sml: diff.behav. [x = -2]";
 
   464 	 | _ => error "rooteq.sml: diff.behav. [x = - 2]";
 
   465 
   465 
   466 "----------- rooteq.sml end--------";
 
   466 "----------- rooteq.sml end--------";
 
   467 
   467 
   468 
   468 
   469 ===== inhibit exn ?===========================================================*)
 
   469 ===== inhibit exn ?===========================================================*)
 
   498 rearrange_assoc*)
 
   498 rearrange_assoc*)
 
   499 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 
   499 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 
   500 (*"9 + 4 * x = 5 + 2 * x + 2 * sqrt (x \<up> 2 + 5 * x)"
 
   500 (*"9 + 4 * x = 5 + 2 * x + 2 * sqrt (x \<up> 2 + 5 * x)"
 
   501 isolate_root*)
 
   501 isolate_root*)
 
   502 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 
   502 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 
   503 (*"sqrt (x \<up> 2 + 5 * x) = (5 + 2 * x + -1 * (9 + 4 * x)) / (-1 * 2)"
 
   503 (*"sqrt (x \<up> 2 + 5 * x) = (5 + 2 * x + - 1 * (9 + 4 * x)) / (- 1 * 2)"
 
   504 Test_simplify*)
 
   504 Test_simplify*)
 
   505 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 
   505 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 
   506 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 
   506 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 
   507 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 
   507 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 
   508 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 
   508 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 
   509 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 
   509 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 
   510 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 
   510 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 
   511 (*"x \<up> 2 + 5 * x + -1 * (4 + (x \<up> 2 + 4 * x)) = 0"*)
 
   511 (*"x \<up> 2 + 5 * x + - 1 * (4 + (x \<up> 2 + 4 * x)) = 0"*)
 
   512 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 
   512 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 
   513 (*"-4 + x = 0"
 
   513 (*"-4 + x = 0"
 
   514   val nxt =("Subproblem",Subproblem ("Test",["LINEAR", "univariate"...*)
 
   514   val nxt =("Subproblem",Subproblem ("Test",["LINEAR", "univariate"...*)
 
   515 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 
   515 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 
   516 (*val nxt =("Model_Problem",Model_Problem ["LINEAR", "univariate"...*)
 
   516 (*val nxt =("Model_Problem",Model_Problem ["LINEAR", "univariate"...*)
 
   524 (*("Specify_Problem",Specify_Problem ["LINEAR", "univariate", "equation"])*)
 
   524 (*("Specify_Problem",Specify_Problem ["LINEAR", "univariate", "equation"])*)
 
   525 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 
   525 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 
   526 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 
   526 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 
   527 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 
   527 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 
   528 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 
   528 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 
   529 (*"x = 0 + -1 * -4", nxt Test_simplify*)
 
   529 (*"x = 0 + - 1 * -4", nxt Test_simplify*)
 
   530 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 
   530 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 
   531 (*"x = 4", nxt Check_Postcond ["LINEAR", "univariate", "equation", "test"]*)
 
   531 (*"x = 4", nxt Check_Postcond ["LINEAR", "univariate", "equation", "test"]*)
 
   532 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 
   532 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 
   533 (*"[x = 4]", nxt Check_elementwise "Assumptions"*)
 
   533 (*"[x = 4]", nxt Check_elementwise "Assumptions"*)
 
   534 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 
   534 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 
   569 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 
   569 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 
   570 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 
   570 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 
   571 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 
   571 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 
   572 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 
   572 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 
   573 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 
   573 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 
   574 (*"9 + -1 * x \<up> 2 = 0"
 
   574 (*"9 + - 1 * x \<up> 2 = 0"
 
   575   Subproblem ("Test",["plain_square", "univariate", "equation"]))*)
 
   575   Subproblem ("Test",["plain_square", "univariate", "equation"]))*)
 
   576 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 
   576 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 
   577 (*Model_Problem ["plain_square", "univariate", "equation"]*)
 
   577 (*Model_Problem ["plain_square", "univariate", "equation"]*)
 
   578 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 
   578 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 
   579 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 
   579 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 
   583 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 
   583 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 
   584 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 
   584 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 
   585 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 
   585 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 
   586 (*Apply_Method ("Test", "solve_plain_square")*)
 
   586 (*Apply_Method ("Test", "solve_plain_square")*)
 
   587 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 
   587 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 
   588 (*"9 + -1 * x \<up> 2 = 0", nxt Rewrite_Set "isolate_bdv"*)
 
   588 (*"9 + - 1 * x \<up> 2 = 0", nxt Rewrite_Set "isolate_bdv"*)
 
   589 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 
   589 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 
   590 (*"x \<up> 2 = (0 + -1 * 9) / -1", nxt Rewrite_Set "Test_simplify"*)
 
   590 (*"x \<up> 2 = (0 + - 1 * 9) / - 1", nxt Rewrite_Set "Test_simplify"*)
 
   591 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 
   591 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 
   592 (*"x \<up> 2 = 9", nxt Rewrite ("square_equality"*)
 
   592 (*"x \<up> 2 = 9", nxt Rewrite ("square_equality"*)
 
   593 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 
   593 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 
   594 (*"x = sqrt 9 | x = -1 * sqrt 9", nxt Rewrite_Set "tval_rls"*)
 
   594 (*"x = sqrt 9 | x = - 1 * sqrt 9", nxt Rewrite_Set "tval_rls"*)
 
   595 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 
   595 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 
   596 (*"x = -3 | x = 3", nxt Or_to_List*)
 
   596 (*"x = -3 | x = 3", nxt Or_to_List*)
 
   597 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 
   597 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 
   598 (*"[x = -3, x = 3]", 
   598 (*"[x = -3, x = 3]", 
   599   nxt Check_Postcond ["plain_square", "univariate", "equation", "test"]*)
 
   599   nxt Check_Postcond ["plain_square", "univariate", "equation", "test"]*)
wneuper/isa