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
branchisac-update-Isa09-2
changeset 37991 028442673981
parent 37986 7b1d2366c191
child 38031 460c24a6a6ba
equal deleted inserted replaced
37990:24609758d219 37991:028442673981 
    86 case result of NoMatch' _  => ()  | _ => raise error "rooteq.sml: new behaviour:";
 
    86 case result of NoMatch' _  => ()  | _ => raise error "rooteq.sml: new behaviour:";
 
    87 
    87 
    88 (*---------rooteq---- 23.8.02 ---------------------*)
 
    88 (*---------rooteq---- 23.8.02 ---------------------*)
 
    89 "---------(1/sqrt(x)=5)---------------------";
 
    89 "---------(1/sqrt(x)=5)---------------------";
 
    90 val fmz = ["equality (1/sqrt(x)=5)","solveFor x","solutions L"];
 
    90 val fmz = ["equality (1/sqrt(x)=5)","solveFor x","solutions L"];
 
    91 val (dI',pI',mI') = ("RootEq.thy",["univariate","equation"],["no_met"]);
 
    91 val (dI',pI',mI') = ("RootEq",["univariate","equation"],["no_met"]);
 
    92 
    92 
    93 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
 
    93 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
 
    94 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 
    94 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 
    95 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 
    95 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 
    96 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 
    96 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 
    97 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 
    97 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 
    98 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 
    98 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 
    99 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 
    99 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 
   100 (*"1 / x = 25" -> Subproblem ("RootEq.thy", ["univariate", ...]) *)
 
   100 (*"1 / x = 25" -> Subproblem ("RootEq", ["univariate", ...]) *)
 
   101 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 
   101 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 
   102 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 
   102 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 
   103 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 
   103 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 
   104 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 
   104 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 
   105 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 
   105 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 
   106 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 
   106 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 
   107 (*"1 = 25 * x" -> Subproblem ("RatEq.thy", ["univariate", ...])*)
 
   107 (*"1 = 25 * x" -> Subproblem ("RatEq", ["univariate", ...])*)
 
   108 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 
   108 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 
   109 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 
   109 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 
   110 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 
   110 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 
   111 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 
   111 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 
   112 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 
   112 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 
   113 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 
   113 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 
   114 if f = Form' (FormKF (~1, EdUndef, 0, Nundef, "1 + -25 * x = 0")) then ()
 
   114 if f = Form' (FormKF (~1, EdUndef, 0, Nundef, "1 + -25 * x = 0")) then ()
 
   115 else raise error "rooteq.sml: diff.behav.poly in (1/sqrt(x)=5)";
 
   115 else raise error "rooteq.sml: diff.behav.poly in (1/sqrt(x)=5)";
 
   116 (*-> Subproblem ("PolyEq.thy", ["polynomial", ...])*)
 
   116 (*-> Subproblem ("PolyEq", ["polynomial", ...])*)
 
   117 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 
   117 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 
   118 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 
   118 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 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 
   121 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 
   135 	     \should be True\n"
 
   135 	     \should be True\n"
 
   136 else raise error "rooteq.sml: diff.behav. with 25 ~= 0";
 
   136 else raise error "rooteq.sml: diff.behav. with 25 ~= 0";
 
   137 
   137 
   138 "---------(sqrt(x+1)=5)---------------------";
 
   138 "---------(sqrt(x+1)=5)---------------------";
 
   139 val fmz = ["equality (sqrt(x+1)=5)","solveFor x","solutions L"];
 
   139 val fmz = ["equality (sqrt(x+1)=5)","solveFor x","solutions L"];
 
   140 val (dI',pI',mI') = ("RootEq.thy",["univariate","equation"],["no_met"]);
 
   140 val (dI',pI',mI') = ("RootEq",["univariate","equation"],["no_met"]);
 
   141 (*val p = e_pos'; 
   141 (*val p = e_pos'; 
   142 val c = []; 
   142 val c = []; 
   143 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
 
   143 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
 
   144 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
 
   144 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
 
   145 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
 
   145 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
 
   147 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 
   147 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 
   148 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 
   148 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 
   149 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 
   149 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 
   150 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 
   150 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 
   151 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 
   151 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 
   152 (*-> Subproblem ("RootEq.thy", ["univariate", ...])*)
 
   152 (*-> Subproblem ("RootEq", ["univariate", ...])*)
 
   153 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 
   153 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 
   154 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 
   154 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 
   155 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 
   155 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 
   156 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 
   156 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 
   157 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 
   157 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 if f = Form' (FormKF (~1, EdUndef, 0, Nundef, "-24 + x = 0")) then ()
 
   159 if f = Form' (FormKF (~1, EdUndef, 0, Nundef, "-24 + x = 0")) then ()
 
   160 else raise error "rooteq.sml: diff.behav.poly in sqrt(x+1)=5";
 
   160 else raise error "rooteq.sml: diff.behav.poly in sqrt(x+1)=5";
 
   161 (*-> Subproblem ("PolyEq.thy", ["polynomial", ...])*)
 
   161 (*-> Subproblem ("PolyEq", ["polynomial", ...])*)
 
   162 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 
   162 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 
   163 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 
   163 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 
   164 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 
   164 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 
   165 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 
   165 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 
   166 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 
   166 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 
   171 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 24]")) => ()
 
   171 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 24]")) => ()
 
   172 	 | _ => raise error "rooteq.sml: diff.behav. [x = 24]";
 
   172 	 | _ => raise error "rooteq.sml: diff.behav. [x = 24]";
 
   173 
   173 
   174 "-------------(4*sqrt(4*x+2)=3*sqrt(2*x+24))-----------------";
 
   174 "-------------(4*sqrt(4*x+2)=3*sqrt(2*x+24))-----------------";
 
   175 val fmz = ["equality (4*sqrt(4*x+2)=3*sqrt(2*x+24))","solveFor x","solutions L"];
 
   175 val fmz = ["equality (4*sqrt(4*x+2)=3*sqrt(2*x+24))","solveFor x","solutions L"];
 
   176 val (dI',pI',mI') = ("RootEq.thy",["univariate","equation"],["no_met"]);
 
   176 val (dI',pI',mI') = ("RootEq",["univariate","equation"],["no_met"]);
 
   177 
   177 
   178 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
 
   178 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
 
   179 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 
   179 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 
   180 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 
   180 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 
   181 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 
   181 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 
   205 	     \should be True\nshould be True\nshould be True\n"
 
   205 	     \should be True\nshould be True\nshould be True\n"
 
   206 else raise error "rooteq.sml: diff.behav. with 0 <= 12 * sqrt 2 * 4";
 
   206 else raise error "rooteq.sml: diff.behav. with 0 <= 12 * sqrt 2 * 4";
 
   207 
   207 
   208 "--------------(sqrt(x+1)+sqrt(4*x+4)=sqrt(9*x+9))----------------";
 
   208 "--------------(sqrt(x+1)+sqrt(4*x+4)=sqrt(9*x+9))----------------";
 
   209 val fmz = ["equality (sqrt(x+1)+sqrt(4*x+4)=sqrt(9*x+9))","solveFor x","solutions L"];
 
   209 val fmz = ["equality (sqrt(x+1)+sqrt(4*x+4)=sqrt(9*x+9))","solveFor x","solutions L"];
 
   210 val (dI',pI',mI') = ("RootEq.thy",["univariate","equation"],["no_met"]);
 
   210 val (dI',pI',mI') = ("RootEq",["univariate","equation"],["no_met"]);
 
   211 
   211 
   212 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
 
   212 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
 
   213 (*val nxt = Model_Problem ["sq","root'","univariate","equation"]) *)
 
   213 (*val nxt = Model_Problem ["sq","root'","univariate","equation"]) *)
 
   214 val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   214 val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   215 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   215 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   217 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   217 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   218 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   218 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   219 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   219 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;
 
   220 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   221 (*"13 + 13 * x + -2 * sqrt ((4 + 4 * x) * (9 + 9 * x)) = 1 + x"))
 
   221 (*"13 + 13 * x + -2 * sqrt ((4 + 4 * x) * (9 + 9 * x)) = 1 + x"))
 
   222 val nxt = ("Subproblem",Subproblem ("RootEq.thy",["univariate","equation"]))*)
 
   222 val nxt = ("Subproblem",Subproblem ("RootEq",["univariate","equation"]))*)
 
   223 val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   223 val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   224 (*val nxt = Model_Problem ["sq","root'","univariate","equation"]) *)
 
   224 (*val nxt = Model_Problem ["sq","root'","univariate","equation"]) *)
 
   225 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   225 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   226 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   226 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   227 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   227 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   228 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   228 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;
 
   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;
 
   231 val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   231 val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   232 (*"144 + 288 * x + 144 * x ^^^ 2 = 144 + x ^^^ 2 + 288 * x + 143 * x ^^^ 2"))
 
   232 (*"144 + 288 * x + 144 * x ^^^ 2 = 144 + x ^^^ 2 + 288 * x + 143 * x ^^^ 2"))
 
   233 val nxt = ("Subproblem",Subproblem ("RootEq.thy",["univariate","equation"]))*)
 
   233 val nxt = ("Subproblem",Subproblem ("RootEq",["univariate","equation"]))*)
 
   234 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   234 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   235 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   235 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   236 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   236 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   237 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   237 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   238 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   238 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   239 val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   239 val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   240 if f = Form' (FormKF (~1, EdUndef, 0, Nundef, "0 = 0")) then ()
 
   240 if f = Form' (FormKF (~1, EdUndef, 0, Nundef, "0 = 0")) then ()
 
   241 else raise error "rooteq.sml: diff.behav.poly in (sqrt(x+1)+sqrt(4*x+4)=sqr..";
 
   241 else raise error "rooteq.sml: diff.behav.poly in (sqrt(x+1)+sqrt(4*x+4)=sqr..";
 
   242 (*-> Subproblem ("PolyEq.thy", ["degree_0", ...])*)
 
   242 (*-> Subproblem ("PolyEq", ["degree_0", ...])*)
 
   243 val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   243 val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   244 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   244 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 c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   245 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   246 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   246 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   247 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   247 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   258 
   258 
   259 "--------------(sqrt(x+1)+sqrt(4*x+4)=sqrt(9*x+9))---------- SUBPBL.2.------";
 
   259 "--------------(sqrt(x+1)+sqrt(4*x+4)=sqrt(9*x+9))---------- SUBPBL.2.------";
 
   260 val fmz = 
   260 val fmz = 
   261     ["equality (13 + 13 * x + -2 * sqrt ((4 + 4 * x) * (9 + 9 * x)) = 1 + x)",
 
   261     ["equality (13 + 13 * x + -2 * sqrt ((4 + 4 * x) * (9 + 9 * x)) = 1 + x)",
 
   262      "solveFor x","solutions L"];
 
   262      "solveFor x","solutions L"];
 
   263 val (dI',pI',mI') = ("RootEq.thy",["sq","root'","univariate","equation"],
 
   263 val (dI',pI',mI') = ("RootEq",["sq","root'","univariate","equation"],
 
   264 		     ["RootEq","solve_sq_root_equation"]);
 
   264 		     ["RootEq","solve_sq_root_equation"]);
 
   265 (*val p = e_pos'; val c = []; 
   265 (*val p = e_pos'; val c = []; 
   266 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
 
   266 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
 
   267 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
 
   267 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
 
   268 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
 
   268 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
 
   272 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 c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   273 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 c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   274 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   274 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   275 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   275 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   276 (*"144 + 288 * x + 144 * x ^^^ 2 = 144 + x ^^^ 2 + 288 * x + 143 * x ^^^ 2"))
 
   276 (*"144 + 288 * x + 144 * x ^^^ 2 = 144 + x ^^^ 2 + 288 * x + 143 * x ^^^ 2"))
 
   277 val nxt = ("Subproblem",Subproblem ("RootEq.thy",["univariate","equation"])) *)
 
   277 val nxt = ("Subproblem",Subproblem ("RootEq",["univariate","equation"])) *)
 
   278 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   278 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   279 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   279 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   280 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   280 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   281 val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   281 val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   282 (*val p = ([6],Pbl)val nxt = Specify_Method ["PolyEq","normalize_poly"])*)
 
   282 (*val p = ([6],Pbl)val nxt = Specify_Method ["PolyEq","normalize_poly"])*)
 
   283 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   283 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   284 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   284 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   285 (*val p = ([6,2],Res) val f = Form' (FormKF (~1,EdUndef,2,Nundef,"0 = 0"))
 
   285 (*val p = ([6,2],Res) val f = Form' (FormKF (~1,EdUndef,2,Nundef,"0 = 0"))
 
   286 val nxt = Subproblem ("PolyEq.thy",["polynomial","univariate","equation"]))*)
 
   286 val nxt = Subproblem ("PolyEq",["polynomial","univariate","equation"]))*)
 
   287 if f = Form' (FormKF (~1, EdUndef, 0, Nundef, "0 = 0")) then ()
 
   287 if f = Form' (FormKF (~1, EdUndef, 0, Nundef, "0 = 0")) then ()
 
   288 else raise error "rooteq.sml: diff.behav.poly in sqrt(x+1)+sqrt(4*x+4)=sqrt..";
 
   288 else raise error "rooteq.sml: diff.behav.poly in sqrt(x+1)+sqrt(4*x+4)=sqrt..";
 
   289 val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   289 val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   290 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 c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   291 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 c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   309 
   309 
   310 (*same error as full expl #######*)
 
   310 (*same error as full expl #######*)
 
   311 
   311 
   312 "--------------(sqrt(x+1)+sqrt(4*x+4)=sqrt(9*x+9))---------- OKversion----";
 
   312 "--------------(sqrt(x+1)+sqrt(4*x+4)=sqrt(9*x+9))---------- OKversion----";
 
   313 val fmz = ["equality (sqrt(x) = 1)","solveFor x","solutions L"];
 
   313 val fmz = ["equality (sqrt(x) = 1)","solveFor x","solutions L"];
 
   314 val (dI',pI',mI') = ("RootEq.thy",["sq","root'","univariate","equation"],
 
   314 val (dI',pI',mI') = ("RootEq",["sq","root'","univariate","equation"],
 
   315 		     ["RootEq","solve_sq_root_equation"]);
 
   315 		     ["RootEq","solve_sq_root_equation"]);
 
   316 (*val p = e_pos'; val c = []; 
   316 (*val p = e_pos'; val c = []; 
   317 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
 
   317 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
 
   318 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
 
   318 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
 
   319 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
 
   319 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
 
   324 (*val p = ([],Pbl)val nxt = Specify_Method ["RootEq","solve_sq_root_equation"*)
 
   324 (*val p = ([],Pbl)val nxt = Specify_Method ["RootEq","solve_sq_root_equation"*)
 
   325 val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   325 val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   326 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   326 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   327 val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   327 val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   328 (* val p = ([2],Res) val f = Form' (FormKF (~1,EdUndef,1,Nundef,"x = 1"))
 
   328 (* val p = ([2],Res) val f = Form' (FormKF (~1,EdUndef,1,Nundef,"x = 1"))
 
   329 val nxt = ("Subproblem",Subproblem ("RootEq.thy",["univariate","equation"]))*)
 
   329 val nxt = ("Subproblem",Subproblem ("RootEq",["univariate","equation"]))*)
 
   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;val (p,_,f,nxt,_,pt) = me nxt p c 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 c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   332 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;
 
   333 val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   334 (*val nxt = ("Specify_Method",Specify_Method ["PolyEq","normalize_poly"])*)
 
   334 (*val nxt = ("Specify_Method",Specify_Method ["PolyEq","normalize_poly"])*)
 
   335 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   335 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   336 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   336 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   337 (*val p = ([3,2],Res)val f = Form' (FormKF (~1,EdUndef,2,Nundef,"-1 + x = 0"))
 
   337 (*val p = ([3,2],Res)val f = Form' (FormKF (~1,EdUndef,2,Nundef,"-1 + x = 0"))
 
   338 val nxt = Subproblem ("PolyEq.thy",["polynomial","univariate","equation"]))*)
 
   338 val nxt = Subproblem ("PolyEq",["polynomial","univariate","equation"]))*)
 
   339 if f = Form' (FormKF (~1, EdUndef, 0, Nundef, "-1 + x = 0")) then ()
 
   339 if f = Form' (FormKF (~1, EdUndef, 0, Nundef, "-1 + x = 0")) then ()
 
   340 else raise error "rooteq.sml: diff.behav.poly in sqrt(x+1)+sqrt(4*x+4)=sqrt..";
 
   340 else raise error "rooteq.sml: diff.behav.poly in sqrt(x+1)+sqrt(4*x+4)=sqrt..";
 
   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;val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   342 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   343 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   343 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   370 
   370 
   371 
   371 
   372 "--------------(sqrt(x+1)+sqrt(4*x+4)=sqrt(9*x+9))---------- SHORTEST.1.----\
 
   372 "--------------(sqrt(x+1)+sqrt(4*x+4)=sqrt(9*x+9))---------- SHORTEST.1.----\
 
   373 \                                                            with same error";
 
   373 \                                                            with same error";
 
   374 val fmz = ["equality (sqrt x = sqrt x)","solveFor x","solutions L"];
 
   374 val fmz = ["equality (sqrt x = sqrt x)","solveFor x","solutions L"];
 
   375 val (dI',pI',mI') = ("RootEq.thy",["sq","root'","univariate","equation"],
 
   375 val (dI',pI',mI') = ("RootEq",["sq","root'","univariate","equation"],
 
   376 		     ["RootEq","solve_sq_root_equation"]);
 
   376 		     ["RootEq","solve_sq_root_equation"]);
 
   377 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
 
   377 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
 
   378 val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   378 val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   379 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   379 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   380 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   380 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   381 val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   381 val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   382 (*val p = ([],Pbl)val nxt = Specify_Method ["RootEq","solve_sq_root_equation"*)
 
   382 (*val p = ([],Pbl)val nxt = Specify_Method ["RootEq","solve_sq_root_equation"*)
 
   383 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   383 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   384 val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   384 val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   385 (*val p = ([1],Res) val f = Form' (FormKF (~1,EdUndef,1,Nundef,"x = x"))
 
   385 (*val p = ([1],Res) val f = Form' (FormKF (~1,EdUndef,1,Nundef,"x = x"))
 
   386 val nxt = ("Subproblem",Subproblem ("RootEq.thy",["univariate","equation"]))*)
 
   386 val nxt = ("Subproblem",Subproblem ("RootEq",["univariate","equation"]))*)
 
   387 val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   387 val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   388 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 c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   389 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 c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   390 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 c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   391 (*val p = ([2],Pbl) val nxt = Specify_Method ["PolyEq","normalize_poly"])*)
 
   391 (*val p = ([2],Pbl) val nxt = Specify_Method ["PolyEq","normalize_poly"])*)
 
   392 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   392 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   393 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   393 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   394 (*val p = ([2,2],Res) val f = Form' (FormKF (~1,EdUndef,2,Nundef,"0 = 0"))
 
   394 (*val p = ([2,2],Res) val f = Form' (FormKF (~1,EdUndef,2,Nundef,"0 = 0"))
 
   395 val nxt = Subproblem ("PolyEq.thy",["polynomial","univariate","equation"]))*)
 
   395 val nxt = Subproblem ("PolyEq",["polynomial","univariate","equation"]))*)
 
   396 if f = Form' (FormKF (~1, EdUndef, 0, Nundef, "0 = 0")) then ()
 
   396 if f = Form' (FormKF (~1, EdUndef, 0, Nundef, "0 = 0")) then ()
 
   397 else raise error "rooteq.sml: diff.behav.poly in sqrt(x+1)+sqrt(4*x+4)=sqrt..";
 
   397 else raise error "rooteq.sml: diff.behav.poly in sqrt(x+1)+sqrt(4*x+4)=sqrt..";
 
   398 val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   398 val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   399 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   399 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   400 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   400 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   418 then () else raise error "new behav. in rooteq.sml: sqrt x = sqrt x";
 
   418 then () else raise error "new behav. in rooteq.sml: sqrt x = sqrt x";
 
   419 
   419 
   420 
   420 
   421 "--------------(3*sqrt(x+3)+sqrt(x+6)=sqrt(4*x+33))----------------";
 
   421 "--------------(3*sqrt(x+3)+sqrt(x+6)=sqrt(4*x+33))----------------";
 
   422 val fmz = ["equality (3*sqrt(x+3)+sqrt(x+6)=sqrt(4*x+33))","solveFor x","solutions L"];
 
   422 val fmz = ["equality (3*sqrt(x+3)+sqrt(x+6)=sqrt(4*x+33))","solveFor x","solutions L"];
 
   423 val (dI',pI',mI') = ("RootEq.thy",["univariate","equation"],["no_met"]);
 
   423 val (dI',pI',mI') = ("RootEq",["univariate","equation"],["no_met"]);
 
   424 
   424 
   425 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
 
   425 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
 
   426 val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   426 val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   427 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 c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   428 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 c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   429 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 c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   430 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   430 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   431 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   431 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   432 val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   432 val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   433 (*        "6 + x = 60 + 13 * x + -6 * sqrt ((3 + x) * (33 + 4 * x))")) : mout
 
   433 (*        "6 + x = 60 + 13 * x + -6 * sqrt ((3 + x) * (33 + 4 * x))")) : mout
 
   434 val nxt = ("Subproblem",Subproblem ("RootEq.thy",["univariate","equation"]))*)
 
   434 val nxt = ("Subproblem",Subproblem ("RootEq",["univariate","equation"]))*)
 
   435 val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   435 val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   436 (*val nxt = Model_Problem ["sq","root'","univariate","equation"]) *)
 
   436 (*val nxt = Model_Problem ["sq","root'","univariate","equation"]) *)
 
   437 val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   437 val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   438 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   438 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   439 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   439 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   440 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   440 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   441 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   441 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   442 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   442 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   443 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   443 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   444 (*"2916 + x ^^^ 2 + 1296 * x + 143 * x ^^^ 2 = 3564 + 1620 * x + 144 * x ^^^ 2"))
 
   444 (*"2916 + x ^^^ 2 + 1296 * x + 143 * x ^^^ 2 = 3564 + 1620 * x + 144 * x ^^^ 2"))
 
   445 val nxt = ("Subproblem",Subproblem ("RootEq.thy",["univariate","equation"]))*)
 
   445 val nxt = ("Subproblem",Subproblem ("RootEq",["univariate","equation"]))*)
 
   446 val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   446 val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   447 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 c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   448 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 c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   449 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 c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   450 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   450 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   451 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   451 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   452 if f = Form' (FormKF (~1, EdUndef, 0, Nundef, "-648 + -324 * x = 0")) then ()
 
   452 if f = Form' (FormKF (~1, EdUndef, 0, Nundef, "-648 + -324 * x = 0")) then ()
 
   453 else raise error "rooteq.sml: diff.behav.poly in 3*sqrt(x+3)+sqrt(x+6)=sqrt..";
 
   453 else raise error "rooteq.sml: diff.behav.poly in 3*sqrt(x+3)+sqrt(x+6)=sqrt..";
 
   454 (*-> Subproblem ("PolyEq.thy", ["degree_1", ...])*)
 
   454 (*-> Subproblem ("PolyEq", ["degree_1", ...])*)
 
   455 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   455 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   456 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   456 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   457 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   457 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;
 
   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;
wneuper/isa