32 CalcTree |
32 CalcTree |
33 [(["equality (x/(x^2 - 6*x+9) - 1/(x^2 - 3*x) =1/x)", |
33 [(["equality (x/(x^2 - 6*x+9) - 1/(x^2 - 3*x) =1/x)", |
34 "solveFor x","solutions L"], |
34 "solveFor x","solutions L"], |
35 ("RatEq",["univariate","equation"],["no_met"]))]; |
35 ("RatEq",["univariate","equation"],["no_met"]))]; |
36 Iterator 1; moveActiveRoot 1; |
36 Iterator 1; moveActiveRoot 1; |
37 autoCalculate' 1 CompleteCalc; |
37 autoCalculate 1 CompleteCalc; |
38 |
38 |
39 getTactic 1 ([1],Res);(*Rewrite_Set RatEq_simplify*) |
39 getTactic 1 ([1],Res);(*Rewrite_Set RatEq_simplify*) |
40 getTactic 1 ([2],Res);(*Rewrite_Set norm_Rational*) |
40 getTactic 1 ([2],Res);(*Rewrite_Set norm_Rational*) |
41 getTactic 1 ([3],Res);(*Rewrite_Set RatEq_eliminate*) |
41 getTactic 1 ([3],Res);(*Rewrite_Set RatEq_eliminate*) |
42 getTactic 1 ([4,1],Res);(*Rewrite all_left*) |
42 getTactic 1 ([4,1],Res);(*Rewrite all_left*) |
226 CalcTree |
226 CalcTree |
227 [(["equality (x/(x^2 - 6*x+9) - 1/(x^2 - 3*x) =1/x)", |
227 [(["equality (x/(x^2 - 6*x+9) - 1/(x^2 - 3*x) =1/x)", |
228 "solveFor x","solutions L"], |
228 "solveFor x","solutions L"], |
229 ("RatEq",["univariate","equation"],["no_met"]))]; |
229 ("RatEq",["univariate","equation"],["no_met"]))]; |
230 Iterator 1; moveActiveRoot 1; |
230 Iterator 1; moveActiveRoot 1; |
231 autoCalculate' 1 CompleteCalc; |
231 autoCalculate 1 CompleteCalc; |
232 val ((pt,_),_) = get_calc 1; |
232 val ((pt,_),_) = get_calc 1; |
233 val p = get_pos 1 1; |
233 val p = get_pos 1 1; |
234 val (Form f, tac, asms) = pt_extract (pt, p); |
234 val (Form f, tac, asms) = pt_extract (pt, p); |
235 if term2str f = "[x = 6 / 5]" andalso p = ([], Res) then () |
235 if term2str f = "[x = 6 / 5]" andalso p = ([], Res) then () |
236 else error "after ===new ptree 2 without changes ==="; |
236 else error "after ===new ptree 2 without changes ==="; |
382 ["LINEAR","univariate","equation","test"], |
382 ["LINEAR","univariate","equation","test"], |
383 ["Test","solve_linear"]))]; |
383 ["Test","solve_linear"]))]; |
384 Iterator 1; moveActiveRoot 1; |
384 Iterator 1; moveActiveRoot 1; |
385 |
385 |
386 (* |
386 (* |
387 autoCalculate' 1 CompleteCalcHead; |
387 autoCalculate 1 CompleteCalcHead; |
388 autoCalculate' 1 (Step 1); |
388 autoCalculate 1 (Step 1); |
389 refFormula 1 (get_pos 1 1); |
389 refFormula 1 (get_pos 1 1); |
390 |
390 |
391 ... works |
391 ... works |
392 |
392 |
393 autoCalculate' 1 CompleteCalcHead; |
393 autoCalculate 1 CompleteCalcHead; |
394 fetchProposedTactic 1; (*-> Apply_Method*); |
394 fetchProposedTactic 1; (*-> Apply_Method*); |
395 setNextTactic 1 (Apply_Method ["Test","solve_linear"]); |
395 setNextTactic 1 (Apply_Method ["Test","solve_linear"]); |
396 autoCalculate' 1 (Step 1); |
396 autoCalculate 1 (Step 1); |
397 refFormula 1 (get_pos 1 1); |
397 refFormula 1 (get_pos 1 1); |
398 |
398 |
399 ... works *) |
399 ... works *) |
400 |
400 |
401 autoCalculate' 1 (Step 1); |
401 autoCalculate 1 (Step 1); |
402 refFormula 1 (get_pos 1 1); |
402 refFormula 1 (get_pos 1 1); |
403 |
403 |
404 autoCalculate' 1 CompleteModel; |
404 autoCalculate 1 CompleteModel; |
405 refFormula 1 (get_pos 1 1); |
405 refFormula 1 (get_pos 1 1); |
406 |
406 |
407 autoCalculate' 1 CompleteCalcHead; |
407 autoCalculate 1 CompleteCalcHead; |
408 (* *** complete_mod: only impl.for Pbl, called with ([], Met) FIXXXXXXXXXXME*) |
408 (* *** complete_mod: only impl.for Pbl, called with ([], Met) FIXXXXXXXXXXME*) |
409 |
409 |
410 |
410 |
411 |
411 |
412 "--------- maximum-example: complete_metitms ---------------------"; |
412 "--------- maximum-example: complete_metitms ---------------------"; |