186 "--------------------- Notlocatable: Free_Solve ---------------------"; |
186 "--------------------- Notlocatable: Free_Solve ---------------------"; |
187 val fmz = []; |
187 val fmz = []; |
188 val (dI',pI',mI') = |
188 val (dI',pI',mI') = |
189 ("Test",["sqroot-test","univariate","equation","test"], |
189 ("Test",["sqroot-test","univariate","equation","test"], |
190 ["Test","sqrt-equ-test"]); |
190 ["Test","sqrt-equ-test"]); |
191 (*val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI'))); |
|
192 val (p,_,f,nxt,_,pt) = me (mI,m) e_pos'[1] EmptyPtree;*) |
|
193 |
|
194 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))]; |
191 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))]; |
195 val nxt = ("Model_Problem", |
192 val nxt = ("Model_Problem", |
196 Model_Problem ["sqroot-test","univariate","equation","test"]); |
193 Model_Problem ["sqroot-test","univariate","equation","test"]); |
197 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
194 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
198 val nxt = |
195 val nxt = |
256 \ (Try (Repeat (Rewrite radd_0)))))\ |
253 \ (Try (Repeat (Rewrite radd_0)))))\ |
257 \ e_e "); |
254 \ e_e "); |
258 atomty sc; |
255 atomty sc; |
259 val (dI',pI',mI') = ("Test",["sqroot-test","univariate","equation","test"], |
256 val (dI',pI',mI') = ("Test",["sqroot-test","univariate","equation","test"], |
260 ["Test","sqrt-equ-test"]); |
257 ["Test","sqrt-equ-test"]); |
261 val p = e_pos'; val c = []; |
258 val c = []; |
262 val (mI,m) = ("Init_Proof",Init_Proof ([], (dI',pI',mI'))); |
259 val (p,_,_,_,_,pt) = CalcTreeTEST [([], (dI',pI',mI')))]; |
263 val (p,_,_,_,_,pt) = me (mI,m) p c EmptyPtree; |
|
264 val nxt = ("Specify_Theory",Specify_Theory "Test"); |
260 val nxt = ("Specify_Theory",Specify_Theory "Test"); |
265 val (p,_,_,_,_,pt) = me nxt p c pt; |
261 val (p,_,_,_,_,pt) = me nxt p c pt; |
266 val nxt = ("Specify_Method",Specify_Method ["Test","sqrt-equ-test"]); (*for asm in square_equation_left*) |
262 val nxt = ("Specify_Method",Specify_Method ["Test","sqrt-equ-test"]); (*for asm in square_equation_left*) |
267 val (p,_,_,_,_,pt) = me nxt p c pt; |
263 val (p,_,_,_,_,pt) = me nxt p c pt; |
268 val p = ([1],Res):pos'; |
264 val p = ([1],Res):pos'; |