(* use"systest/auto-inform.sml";

   use"auto-inform.sml";

   *)

"autoCalculate"; 

"--------- solve_linear as rootpbl AUTOCALCULATE CompleteModel ---";

"--------- solve_linear as rootpbl AUTOCALCULATE CompleteCalcHead-";

"--------- maximum-example: complete_metitms ---------------------";

"--------- maximum-example: complete_mod -------------------------";

"appendForm with miniscript with mini-subpbl:";

"--------- appendFormula: on Res + equ_nrls ----------------------";

"--------- appendFormula: on Frm + equ_nrls ----------------------";

"--------- appendFormula: on Res + NO deriv ----------------------";

"--------- appendFormula: on Res + late deriv --------------------";

"--------- appendFormula: on Res + late deriv [x = 3 + -2]---///--";

"replaceForm with miniscript with mini-subpbl:";

"--------- replaceFormula: on Res + = ----------------------------";

"--------- replaceFormula: on Res + = 1st Nd ---------------------";

"--------- replaceFormula: on Frm + = 1st Nd ---------------------";

"--------- replaceFormula: cut calculation -----------------------";

"--------- solve_linear as rootpbl AUTOCALCULATE CompleteModel ---";

"--------- solve_linear as rootpbl AUTOCALCULATE CompleteModel ---";

"--------- solve_linear as rootpbl AUTOCALCULATE CompleteModel ---";

 val c = [];

 val (p,_,f,nxt,_,pt) = CalcTreeTEST 

     [(["equality (1+-1*2+x=0)", "solveFor x","solutions L"],

       ("Test.thy", 

	["linear","univariate","equation","test"],

	["Test","solve_linear"]))];

 val (p,_,f,nxt,_,pt) = me nxt p c pt;

 val (p,_,f,nxt,_,pt) = me nxt p c pt;

 (*xt = Add_Given "solveFor x"*)

 writeln (itms2str thy (get_obj g_pbl pt (fst p)));   

(*[

(0 ,[] ,false ,#Given ,Inc solveFor ,(??.empty, [])),

(0 ,[] ,false ,#Find ,Inc solutions [] ,(??.empty, [])),

(1 ,[1] ,true ,#Given ,Cor equality (1 + -1 * 2 + x = 0) ,(e_, [1 + -1 * 2 + x = 0]))]*)

 val (pt,p) = complete_mod (pt, p);

 if itms2str thy (get_obj g_pbl pt (fst p)) = "[\n(1 ,[1] ,true ,#Given ,Cor equality (1 + -1 * 2 + x = 0) ,(e_, [1 + -1 * 2 + x = 0])),\n(2 ,[1] ,true ,#Given ,Cor solveFor x ,(v_, [x])),\n(3 ,[1] ,true ,#Find ,Cor solutions L ,(v_i_, [L]))]" then ()

 else raise error "completetest.sml: new behav. in complete_mod 1";

 writeln (itms2str thy (get_obj g_pbl pt (fst p)));   

(*[

(1 ,[1] ,true ,#Given ,Cor equality (1 + -1 * 2 + x = 0) ,(e_, [1 + -1 * 2 + x = 0])),

(2 ,[1] ,true ,#Given ,Cor solveFor x ,(solveFor, [x])),

(3 ,[1] ,true ,#Find ,Cor solutions L ,(solutions, [L]))]*)

 val mits = get_obj g_met pt (fst p);

 if itms2str thy mits = "[\n(1 ,[1] ,true ,#Given ,Cor equality (1 + -1 * 2 + x = 0) ,(e_, [1 + -1 * 2 + x = 0])),\n(2 ,[1] ,true ,#Given ,Cor solveFor x ,(v_, [x])),\n(3 ,[1] ,true ,#Find ,Cor solutions L ,(v_i_, [L]))]" 

 then () else raise error "completetest.sml: new behav. in complete_mod 2";

 writeln (itms2str thy mits);   

(*[

(1 ,[1] ,true ,#Given ,Cor equality (1 + -1 * 2 + x = 0) ,(e_, [1 + -1 * 2 + x = 0])),

(2 ,[1] ,true ,#Given ,Cor solveFor x ,(solveFor, [x])),

(3 ,[1] ,true ,#Find ,Cor solutions L ,(solutions, [L]))]*)

"--------- solve_linear as rootpbl AUTOCALCULATE CompleteCalcHead-";

"--------- solve_linear as rootpbl AUTOCALCULATE CompleteCalcHead-";

"--------- solve_linear as rootpbl AUTOCALCULATE CompleteCalcHead-";

 states:=[];

 CalcTree      (*start of calculation, return No.1*)

     [(["equality (1+-1*2+x=0)", "solveFor x","solutions L"],

       ("Test.thy", 

	["linear","univariate","equation","test"],

	["Test","solve_linear"]))];

 Iterator 1; moveActiveRoot 1;

(* 

 autoCalculate 1 CompleteCalcHead;

 autoCalculate 1 (Step 1); 

 refFormula 1 1; 

... works 

 autoCalculate 1 CompleteCalcHead;

 fetchProposedTactic 1; (*-> Apply_Method*);

 setNextTactic 1 (Apply_Method ["Test","solve_linear"]);

 autoCalculate 1 (Step 1); 

 refFormula 1 1; 

... works *)

 autoCalculate 1 (Step 1); 

 refFormula 1 (get_pos 1 1);

 autoCalculate 1 CompleteModel;

 refFormula 1 (get_pos 1 1);

 autoCalculate 1 CompleteCalcHead;

(* *** complete_mod: only impl.for Pbl, called with ([], Met) FIXXXXXXXXXXME*)

"--------- maximum-example: complete_metitms ---------------------";

"--------- maximum-example: complete_metitms ---------------------";

"--------- maximum-example: complete_metitms ---------------------";

 val (p,_,f,nxt,_,pt) = 

     CalcTreeTEST 

     [(["fixedValues [r=Arbfix]","maximum A",

	"valuesFor [a,b]",

	"relations [A=a*b, (a/2)^^^2 + (b/2)^^^2 = r^^^2]",

	"relations [A=a*b, (a/2)^^^2 + (b/2)^^^2 = r^^^2]",

	"relations [A=a*b, a/2=r*sin alpha, b/2=r*cos alpha]",

	"boundVariable a","boundVariable b","boundVariable alpha",

	"interval {x::real. 0 <= x & x <= 2*r}",

	"interval {x::real. 0 <= x & x <= 2*r}",

	"interval {x::real. 0 <= x & x <= pi}",

	"errorBound (eps=(0::real))"],

       ("DiffApp.thy",["maximum_of","function"],["DiffApp","max_by_calculus"])

       )];

 val (p,_,f,nxt,_,pt) = me nxt p c pt;

 val (p,_,f,nxt,_,pt) = me nxt p c pt;

 val (p,_,f,nxt,_,pt) = me nxt p c pt;

 val (p,_,f,nxt,_,pt) = me nxt p c pt;

 val (p,_,f,nxt,_,pt) = (me nxt p c pt) handle e => print_exn e;

 val (p,_,f,nxt,_,pt) = me nxt p c pt;

 val (p,_,f,nxt,_,pt) = me nxt p c pt;

 (*nxt = Specify_Theory "DiffApp.thy"*)

 val (oris, _, _) = get_obj g_origin pt (fst p);

 writeln (oris2str oris);

(*[

(1, ["1","2","3"], #Given,fixedValues, ["[r = Arbfix]"]),

(2, ["1","2","3"], #Find,maximum, ["A"]),

(3, ["1","2","3"], #Find,valuesFor, ["[a]","[b]"]),

(4, ["1","2"], #Relate,relations, ["[A = a * b]","[(a / 2) ^^^ 2 + (b / 2) ^^^ 2 = r ^^^ 2]"]),

(5, ["3"], #Relate,relations, ["[A = a * b]","[a / 2 = r * sin alpha]","[b / 2 = r * cos alpha]"]),

(6, ["1"], #undef,boundVariable, ["a"]),

(7, ["2"], #undef,boundVariable, ["b"]),

(8, ["3"], #undef,boundVariable, ["alpha"]),

(9, ["1","2"], #undef,interval, ["{x. 0 <= x & x <= 2 * r}"]),

(10, ["3"], #undef,interval, ["{x. 0 <= x & x <= pi}"]),

(11, ["1","2","3"], #undef,errorBound, ["eps = 0"])]*)

 val pits = get_obj g_pbl pt (fst p);

 writeln (itms2str thy pits);

(*[

(1 ,[1,2,3] ,true,#Given ,Cor fixedValues [r = Arbfix],(fix_, [[r = Arbfix]])),

(2 ,[1,2,3] ,true,#Find ,Cor maximum A ,(m_, [A])),

(3 ,[1,2,3] ,true,#Find ,Cor valuesFor [a, b] ,(vs_, [[a, b]])),

(4 ,[1,2] ,true,#Relate ,Cor relations [A = a * b, (a / 2) ^^^ 2 + (b / 2) ^^^

2 = r ^^^ 2] ,(rs_, [[A = a * b, (a / 2) ^^^ 2 + (b / 2) ^^^ 2 = r ^^^ 2]]))]*)

 val mits = get_obj g_met pt (fst p);

 val mits = complete_metitms oris pits [] 

			((#ppc o get_met) ["DiffApp","max_by_calculus"]);

 writeln (itms2str thy mits);

(*[

(1 ,[1,2,3] ,true ,#Given ,Cor fixedValues [r = Arbfix] ,(fix_, [[r = Arbfix]])),

(2 ,[1,2,3] ,true ,#Find ,Cor maximum A ,(m_, [A])),

(3 ,[1,2,3] ,true ,#Find ,Cor valuesFor [a, b] ,(vs_, [[a, b]])),

(4 ,[1,2] ,true ,#Relate ,Cor relations [A = a * b, (a / 2) ^^^ 2 + (b / 2) ^^^

2 = r ^^^ 2] ,(rs_, [[A = a * b, (a / 2) ^^^ 2 + (b / 2) ^^^ 2 = r ^^^ 2]])),

(6 ,[1] ,true ,#undef ,Cor boundVariable a ,(boundVariable, [a])),

(9 ,[1,2] ,true ,#undef ,Cor interval {x. 0 <= x & x <= 2 * r} ,(interval, [{x.

0 <= x & x <= 2 * r}])),

(11 ,[1,2,3] ,true ,#undef ,Cor errorBound (eps = 0) ,(errorBound, [eps = 0]))]*)

 if itms2str thy mits = "[\n(1 ,[1,2,3] ,true ,#Given ,Cor fixedValues [r = Arbfix] ,(fix_, [[r = Arbfix]])),\n(2 ,[1,2,3] ,true ,#Find ,Cor maximum A ,(m_, [A])),\n(3 ,[1,2,3] ,true ,#Find ,Cor valuesFor [a, b] ,(vs_, [[a, b]])),\n(4 ,[1,2] ,true ,#Relate ,Cor relations [A = a * b, (a / 2) ^^^ 2 + (b / 2) ^^^ 2 = r ^^^ 2] ,(rs_, [[A = a * b, (a / 2) ^^^ 2 + (b / 2) ^^^ 2 = r ^^^ 2]])),\n(6 ,[1] ,true ,#undef ,Cor boundVariable a ,(v_, [a])),\n(9 ,[1,2] ,true ,#undef ,Cor interval {x. 0 <= x & x <= 2 * r} ,(itv_, [{x. 0 <= x & x <= 2 * r}])),\n(11 ,[1,2,3] ,true ,#undef ,Cor errorBound (eps = 0) ,(err_, [eps = 0]))]" then ()

 else raise error "completetest.sml: new behav. in complete_metitms 1";

"--------- maximum-example: complete_mod -------------------------";

"--------- maximum-example: complete_mod -------------------------";

"--------- maximum-example: complete_mod -------------------------";

 val (p,_,f,nxt,_,pt) = 

     CalcTreeTEST 

     [(["fixedValues [r=Arbfix]","maximum A",

	"valuesFor [a,b]",

	"relations [A=a*b, (a/2)^^^2 + (b/2)^^^2 = r^^^2]",

	"relations [A=a*b, (a/2)^^^2 + (b/2)^^^2 = r^^^2]",

	"relations [A=a*b, a/2=r*sin alpha, b/2=r*cos alpha]",

	"boundVariable a","boundVariable b","boundVariable alpha",

	"interval {x::real. 0 <= x & x <= 2*r}",

	"interval {x::real. 0 <= x & x <= 2*r}",

	"interval {x::real. 0 <= x & x <= pi}",

	"errorBound (eps=(0::real))"],

       ("DiffApp.thy",["maximum_of","function"],["DiffApp","max_by_calculus"])

       )];

 val (p,_,f,nxt,_,pt) = me nxt p c pt;

 val (p,_,f,nxt,_,pt) = me nxt p c pt;

 val (p,_,f,nxt,_,pt) = me nxt p c pt;

 (*nxt = nxt = Add_Find "valuesFor [a]" FIXME.12.03 +handle Inc !*)

 val pits = get_obj g_pbl pt (fst p);

 writeln (itms2str thy pits);

(*[

(0 ,[] ,false ,#Find ,Inc valuesFor ,(??.empty, [])),

(0 ,[] ,false ,#Relate ,Inc relations [] ,(??.empty, [])),

(1 ,[1,2,3] ,true,#Given,Cor fixedValues [r = Arbfix] ,(fix_, [[r = Arbfix]])),

(2 ,[1,2,3] ,true ,#Find ,Cor maximum A ,(m_, [A]))]*) 

 val (pt,p) = complete_mod (pt,p);

 val pits = get_obj g_pbl pt (fst p);

 if itms2str thy pits = "[\n(1 ,[1,2,3] ,true ,#Given ,Cor fixedValues [r = Arbfix] ,(fix_, [[r = Arbfix]])),\n(2 ,[1,2,3] ,true ,#Find ,Cor maximum A ,(m_, [A])),\n(3 ,[1,2,3] ,true ,#Find ,Cor valuesFor [a, b] ,(vs_, [[a],[b]])),\n(4 ,[1,2] ,true ,#Relate ,Cor relations [A = a * b, (a / 2) ^^^ 2 + (b / 2) ^^^ 2 = r ^^^ 2] ,(rs_, [[A = a * b],[(a / 2) ^^^ 2 + (b / 2) ^^^ 2 = r ^^^ 2]]))]" 

 then () else raise error "completetest.sml: new behav. in complete_mod 3";

 writeln (itms2str thy pits);

(*[

(1 ,[1,2,3] ,true,#Given,Cor fixedValues [r = Arbfix] ,(fix_, [[r = Arbfix]])),

(2 ,[1,2,3] ,true ,#Find ,Cor maximum A ,(m_, [A])),

(3 ,[1,2,3] ,true ,#Find ,Cor valuesFor [a, b] ,(valuesFor, [[a],[b]])),

(4 ,[1,2] ,true ,#Relate ,Cor relations [A = a * b, (a / 2) ^^^ 2 + (b / 2) ^^^

2 = r ^^^ 2] ,(relations, [[A = a * b],[(a / 2) ^^^ 2 + (b / 2) ^^^ 2 = r ^^^ 2]]))]*)

 val mits = get_obj g_met pt (fst p);

 if itms2str thy mits = "[\n(1 ,[1,2,3] ,true ,#Given ,Cor fixedValues [r = Arbfix] ,(fix_, [[r = Arbfix]])),\n(2 ,[1,2,3] ,true ,#Find ,Cor maximum A ,(m_, [A])),\n(3 ,[1,2,3] ,true ,#Find ,Cor valuesFor [a, b] ,(vs_, [[a],[b]])),\n(4 ,[1,2] ,true ,#Relate ,Cor relations [A = a * b, (a / 2) ^^^ 2 + (b / 2) ^^^ 2 = r ^^^ 2] ,(rs_, [[A = a * b],[(a / 2) ^^^ 2 + (b / 2) ^^^ 2 = r ^^^ 2]])),\n(6 ,[1] ,true ,#undef ,Cor boundVariable a ,(v_, [a])),\n(9 ,[1,2] ,true ,#undef ,Cor interval {x. 0 <= x & x <= 2 * r} ,(itv_, [{x. 0 <= x & x <= 2 * r}])),\n(11 ,[1,2,3] ,true ,#undef ,Cor errorBound (eps = 0) ,(err_, [eps = 0]))]" 

 then () else raise error "completetest.sml: new behav. in complete_mod 3";

 writeln (itms2str thy mits);

(*[

(1 ,[1,2,3] ,true ,#Given ,Cor fixedValues [r = Arbfix] ,(fix_, [[r = Arbfix]])),

(2 ,[1,2,3] ,true ,#Find ,Cor maximum A ,(m_, [A])),

(3 ,[1,2,3] ,true ,#Find ,Cor valuesFor [a, b] ,(valuesFor, [[a],[b]])),

(4 ,[1,2] ,true ,#Relate ,Cor relations [A = a * b, (a / 2) ^^^ 2 + (b / 2) ^^^

2 = r ^^^ 2] ,(relations, [[A = a * b],[(a / 2) ^^^ 2 + (b / 2) ^^^ 2 = r ^^^ 2]])),

(6 ,[1] ,true ,#undef ,Cor boundVariable a ,(boundVariable, [a])),

(9 ,[1,2] ,true ,#undef ,Cor interval {x. 0 <= x & x <= 2 * r} ,(interval, [{x.

0 <= x & x <= 2 * r}])),

(11 ,[1,2,3] ,true ,#undef ,Cor errorBound (eps = 0) ,(errorBound, [eps = 0]))]*)

"--------- appendFormula: on Res + equ_nrls ----------------------";

"--------- appendFormula: on Res + equ_nrls ----------------------";

"--------- appendFormula: on Res + equ_nrls ----------------------";

 val Script sc = (#scr o get_met) ["Test","squ-equ-test-subpbl1"];

 (writeln o term2str) sc;

 val Script sc = (#scr o get_met) ["Test","solve_linear"];

 (writeln o term2str) sc;

 states:=[];

 CalcTree [(["equality (x+1=2)", "solveFor x","solutions L"], 

	    ("Test.thy", 

	     ["sqroot-test","univariate","equation","test"],

	     ["Test","squ-equ-test-subpbl1"]))];

 Iterator 1; moveActiveRoot 1;

 autoCalculate 1 CompleteCalcHead;

 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);(*x + 1 = 2*)

 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);(*x + 1 + -1 * 2 = 0*);

 appendFormula 1 "-2 * 1 + (1 + x) = 0"; refFormula 1 (get_pos 1 1);

 val ((pt,_),_) = get_calc 1;

 val str = pr_ptree pr_short pt;

 writeln str;

 if str = ".    ----- pblobj -----\n1.   x + 1 = 2\n2.   x + 1 + -1 * 2 = 0\n2.1.   x + 1 + -1 * 2 = 0\n2.2.   -1 * 2 + (x + 1) = 0\n2.3.   -1 * 2 + (1 + x) = 0\n2.4.   1 + (-1 * 2 + x) = 0\n2.5.   1 + (-2 + x) = 0\n2.6.   1 + (-2 * 1 + x) = 0\n" then ()

 else raise error "auto-inform.sml: diff.behav.appendFormula: on Res + equ 1";

 moveDown 1 ([ ],Pbl); refFormula 1 ([1],Frm); (*x + 1 = 2*)

 moveDown 1 ([1],Frm); refFormula 1 ([1],Res); (*x + 1 + -1 * 2 = 0*)

 (*the seven steps of detailed derivation*)

 moveDown 1 ([1  ],Res); refFormula 1 ([2,1],Frm); 

 moveDown 1 ([2,1],Frm); refFormula 1 ([2,1],Res);

 moveDown 1 ([2,1],Res); refFormula 1 ([2,2],Res);

 moveDown 1 ([2,2],Res); refFormula 1 ([2,3],Res); 

 moveDown 1 ([2,3],Res); refFormula 1 ([2,4],Res);

 moveDown 1 ([2,4],Res); refFormula 1 ([2,5],Res);

 moveDown 1 ([2,5],Res); refFormula 1 ([2,6],Res);

 val ((pt,_),_) = get_calc 1;

 if "-2 * 1 + (1 + x) = 0" = term2str (fst (get_obj g_result pt [2,6])) then()

 else raise error "auto-inform.sml: diff.behav.appendFormula: on Res + equ 2";

 fetchProposedTactic 1; (*takes Iterator 1 _1_*)

 val (_,(tac,_,_)::_) = get_calc 1;

 if tac = Rewrite_Set "Test_simplify" then ()

 else raise error "auto-inform.sml: diff.behav.appendFormula: on Res + equ 3";

 autoCalculate 1 CompleteCalc;

 val ((pt,_),_) = get_calc 1;

 if "[x = 1]" = term2str (fst (get_obj g_result pt [])) then ()

 else raise error "auto-inform.sml: diff.behav.appendFormula: on Res + equ 4";

 (* autoCalculate 1 CompleteCalc;

   val ((pt,p),_) = get_calc 1;

   (writeln o istates2str) (get_obj g_loc pt [ ]);  

   (writeln o istates2str) (get_obj g_loc pt [1]);  

   (writeln o istates2str) (get_obj g_loc pt [2]);  

   (writeln o istates2str) (get_obj g_loc pt [3]);  

   (writeln o istates2str) (get_obj g_loc pt [3,1]);  

   (writeln o istates2str) (get_obj g_loc pt [3,2]);  

   (writeln o istates2str) (get_obj g_loc pt [4]);  

   *)

"----------------------------------------------------------";

 val fod = make_deriv Isac.thy Atools_erls 

		       ((#rules o rep_rls) Test_simplify)

		       (sqrt_right false ProtoPure.thy) None 

		       (str2term "x + 1 + -1 * 2 = 0");

 (writeln o trtas2str) fod;

 val ifod = make_deriv Isac.thy Atools_erls 

		       ((#rules o rep_rls) Test_simplify)

		       (sqrt_right false ProtoPure.thy) None 

		       (str2term "-2 * 1 + (1 + x) = 0");

 (writeln o trtas2str) ifod;

 fun equal (_,_,(t1, _)) (_,_,(t2, _)) = t1=t2;

 val (fod', rifod') = dropwhile' equal (rev fod) (rev ifod);

 val der = fod' @ (map rev_deriv' rifod');

 (writeln o trtas2str) der;

 "----------------------------------------------------------";

"--------- appendFormula: on Frm + equ_nrls ----------------------";

"--------- appendFormula: on Frm + equ_nrls ----------------------";

"--------- appendFormula: on Frm + equ_nrls ----------------------";

 states:=[];

 CalcTree [(["equality (x+1=2)", "solveFor x","solutions L"], 

	    ("Test.thy", 

	     ["sqroot-test","univariate","equation","test"],

	     ["Test","squ-equ-test-subpbl1"]))];

 Iterator 1; moveActiveRoot 1;

 autoCalculate 1 CompleteCalcHead;

 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1) (*x + 1 = 2*);

 appendFormula 1 "2+ -1 + x = 2"; refFormula 1 (get_pos 1 1);

 moveDown 1 ([],Pbl); refFormula 1 ([1],Frm) (*x + 1 = 2*);

 moveDown 1 ([1  ],Frm); refFormula 1 ([1,1],Frm); 

 moveDown 1 ([1,1],Frm); refFormula 1 ([1,1],Res); 

 moveDown 1 ([1,1],Res); refFormula 1 ([1,2],Res); 

 moveDown 1 ([1,2],Res); refFormula 1 ([1,3],Res); 

 moveDown 1 ([1,3],Res); refFormula 1 ([1,4],Res); 

 moveDown 1 ([1,4],Res); refFormula 1 ([1,5],Res); 

 moveDown 1 ([1,5],Res); refFormula 1 ([1,6],Res); 

 val ((pt,_),_) = get_calc 1;

 if "2 + -1 + x = 2" = term2str (fst (get_obj g_result pt [1,6])) then()

 else raise error "auto-inform.sml: diff.behav.appendFormula: on Frm + equ 1";

 fetchProposedTactic 1; (*takes Iterator 1 _1_*)

 val (_,(tac,_,_)::_) = get_calc 1;

 if tac = Rewrite_Set "norm_equation" then ()

 else raise error "auto-inform.sml: diff.behav.appendFormula: on Frm + equ 2";

 autoCalculate 1 CompleteCalc;

 val ((pt,_),_) = get_calc 1;

 if "[x = 1]" = term2str (fst (get_obj g_result pt [])) then ()

 else raise error "auto-inform.sml: diff.behav.appendFormula: on Frm + equ 3";

"--------- appendFormula: on Res + NO deriv ----------------------";

"--------- appendFormula: on Res + NO deriv ----------------------";

"--------- appendFormula: on Res + NO deriv ----------------------";

 states:=[];

 CalcTree [(["equality (x+1=2)", "solveFor x","solutions L"], 

	    ("Test.thy", 

	     ["sqroot-test","univariate","equation","test"],

	     ["Test","squ-equ-test-subpbl1"]))];

 Iterator 1; moveActiveRoot 1;

 autoCalculate 1 CompleteCalcHead;

 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);(*x + 1 = 2*)

 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);(*x + 1 + -1 * 2 = 0*);

 appendFormula 1 "x = 2";

 val ((pt,p),_) = get_calc 1;

 val str = pr_ptree pr_short pt;

 writeln str;

 if str = ".    ----- pblobj -----\n1.   x + 1 = 2\n" andalso p = ([1], Res)

 then ()

 else raise error "auto-inform.sml: diff.behav.appendFormula: Res + NOder 1";

 fetchProposedTactic 1;

 val (_,(tac,_,_)::_) = get_calc 1;

 if tac = Rewrite_Set "Test_simplify" then ()

 else raise error "auto-inform.sml: diff.behav.appendFormula: Res + NOder 2";

 autoCalculate 1 CompleteCalc;

 val ((pt,_),_) = get_calc 1;

 if "[x = 1]" = term2str (fst (get_obj g_result pt [])) then ()

 else raise error "auto-inform.sml: diff.behav.appendFormula: on Frm + equ 3";

"--------- appendFormula: on Res + late deriv --------------------";

"--------- appendFormula: on Res + late deriv --------------------";

"--------- appendFormula: on Res + late deriv --------------------";

 states:=[];

 CalcTree [(["equality (x+1=2)", "solveFor x","solutions L"], 

	    ("Test.thy", 

	     ["sqroot-test","univariate","equation","test"],

	     ["Test","squ-equ-test-subpbl1"]))];

 Iterator 1; moveActiveRoot 1;

 autoCalculate 1 CompleteCalcHead;

 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);(*x + 1 = 2*)

 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);(*x + 1 + -1 * 2 = 0*);

 appendFormula 1 "x = 1";

 val ((pt,p),_) = get_calc 1;

 val str = pr_ptree pr_short pt;

 writeln str;

 if str = ".    ----- pblobj -----\n1.   x + 1 = 2\n2.   x + 1 + -1 * 2 = 0\n3.    ----- pblobj -----\n3.1.   -1 + x = 0\n3.2.   x = 0 + -1 * -1\n3.2.1.   x = 0 + -1 * -1\n3.2.2.   x = 0 + 1\n" andalso p = ([3,2], Res)

 then () (*finds 1 step too early: ([3,2], Res) "x = 1" also by script !!!*)

 else raise error "auto-inform.sml: diff.behav.appendFormula: Res + late d 1";

 fetchProposedTactic 1;

 val (_,(tac,_,_)::_) = get_calc 1;

 if tac = Check_Postcond ["linear", "univariate", "equation", "test"] then ()

 else raise error "auto-inform.sml: diff.behav.appendFormula: Res + late d 2";

 autoCalculate 1 CompleteCalc;

 val ((pt,_),_) = get_calc 1;

 if "[x = 1]" = term2str (fst (get_obj g_result pt [])) then ()

 else raise error "auto-inform.sml: diff.behav.appendFormula: Res + late d 3";

"--------- appendFormula: on Res + late deriv [x = 3 + -2]---///--";

"--------- appendFormula: on Res + late deriv [x = 3 + -2]---///--";

"--------- appendFormula: on Res + late deriv [x = 3 + -2]---///--";

 states:=[];

 CalcTree [(["equality (x+1=2)", "solveFor x","solutions L"], 

	    ("Test.thy", 

	     ["sqroot-test","univariate","equation","test"],

	     ["Test","squ-equ-test-subpbl1"]))];

 Iterator 1; moveActiveRoot 1;

 autoCalculate 1 CompleteCalcHead;

 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);(*x + 1 = 2*)

 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);(*x + 1 + -1 * 2 = 0*);

 appendFormula 1 "[x = 3 + -2*1]";

 val ((pt,p),_) = get_calc 1;

 val str = pr_ptree pr_short pt;

 writeln str;

 if str=".    ----- pblobj -----\n1.   x + 1 = 2\n2.   x + 1 + -1 * 2 = 0\n3.    ----- pblobj -----\n3.1.   -1 + x = 0\n3.2.   x = 0 + -1 * -1\n4.   [x = 1]\n4.1.   [x = 1]\n4.2.   [x = -2 + 3]\n4.3.   [x = 3 + -2]\n" then ()

 else raise error "auto-inform.sml: diff.behav.appendFormula: Res + latEE 1";

 autoCalculate 1 CompleteCalc;

 val ((pt,p),_) = get_calc 1;

 if "[x = 3 + -2 * 1]" = term2str (fst (get_obj g_result pt [])) then ()

 (*       ~~~~~~~~~~ simplify as last step in any script ?!*)

 else raise error "auto-inform.sml: diff.behav.appendFormula: Res + latEE 2";

"--------- replaceFormula: on Res + = ----------------------------";

"--------- replaceFormula: on Res + = ----------------------------";

"--------- replaceFormula: on Res + = ----------------------------";

 states:=[];

 CalcTree [(["equality (x+1=2)", "solveFor x","solutions L"], 

	    ("Test.thy", 

	     ["sqroot-test","univariate","equation","test"],

	     ["Test","squ-equ-test-subpbl1"]))];

 Iterator 1; moveActiveRoot 1;

 autoCalculate 1 CompleteCalcHead;

 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);(*x + 1 = 2*)

 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);(*x + 1 + -1 * 2 = 0*);

 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);(*-1 + x*);

 replaceFormula 1 "-2 * 1 + (1 + x) = 0"; refFormula 1 (get_pos 1 1);

 val ((pt,_),_) = get_calc 1;

 val str = pr_ptree pr_short pt;

 writeln str;

 if str=".    ----- pblobj -----\n1.   x + 1 = 2\n2.   x + 1 + -1 * 2 = 0\n2.1.   x + 1 + -1 * 2 = 0\n2.2.   -1 * 2 + (x + 1) = 0\n2.3.   -1 * 2 + (1 + x) = 0\n2.4.   1 + (-1 * 2 + x) = 0\n2.5.   1 + (-2 + x) = 0\n2.6.   1 + (-2 * 1 + x) = 0\n" then()

 else raise error "auto-inform.sml: diff.behav.replaceFormula: on Res += 1";

 autoCalculate 1 CompleteCalc;

 val ((pt,pos as(p,_)),_) = get_calc 1;

 if pos=([],Res)andalso"[x = 1]"=(term2str o fst)(get_obj g_result pt p)then()

 else raise error "auto-inform.sml: diff.behav.replaceFormula: on Res + = 2";

"--------- replaceFormula: on Res + = 1st Nd ---------------------";

"--------- replaceFormula: on Res + = 1st Nd ---------------------";

"--------- replaceFormula: on Res + = 1st Nd ---------------------";

 states:=[];

 CalcTree [(["equality (x+1=2)", "solveFor x","solutions L"], 

	    ("Test.thy", 

	     ["sqroot-test","univariate","equation","test"],

	     ["Test","squ-equ-test-subpbl1"]))];

 Iterator 1; moveActiveRoot 1;

 autoCalculate 1 CompleteCalcHead;

 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);(*x + 1 = 2*)

 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);(*x + 1 + -1 * 2 = 0*);

 replaceFormula 1 "x + 1 = 4 + -2"; refFormula 1 (get_pos 1 1);

 val ((pt,_),_) = get_calc 1;

 val str = pr_ptree pr_short pt;

 writeln str;

 if str=".    ----- pblobj -----\n1.   x + 1 = 2\n1.1.   x + 1 = 2\n1.2.   1 + x = 2\n1.3.   1 + x = -2 + 4\n1.4.   x + 1 = -2 + 4\n" then ()

 else raise error "auto-inform.sml: diff.behav.replaceFormula: on Res 1 + = 1";

 autoCalculate 1 CompleteCalc;

 val ((pt,pos as(p,_)),_) = get_calc 1;

 if pos=([],Res)andalso"[x = 1]"=(term2str o fst)(get_obj g_result pt p)then()

 else raise error "auto-inform.sml: diff.behav.replaceFormula: on Res + = 2";

"--------- replaceFormula: on Frm + = 1st Nd ---------------------";

"--------- replaceFormula: on Frm + = 1st Nd ---------------------";

"--------- replaceFormula: on Frm + = 1st Nd ---------------------";

 states:=[];

 CalcTree [(["equality (x+1=2)", "solveFor x","solutions L"], 

	    ("Test.thy", 

	     ["sqroot-test","univariate","equation","test"],

	     ["Test","squ-equ-test-subpbl1"]))];

 Iterator 1; moveActiveRoot 1;

 autoCalculate 1 CompleteCalcHead;

 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);(*x + 1 = 2*)

 replaceFormula 1 "x + 1 = 4 + -2"; refFormula 1 (get_pos 1 1);

 val ((pt,_),_) = get_calc 1;

 val str = pr_ptree pr_short pt;

 writeln str;

 if str=".    ----- pblobj -----\n1.   x + 1 = 2\n1.1.   x + 1 = 2\n1.2.   1 + x = 2\n1.3.   1 + x = -2 + 4\n1.4.   x + 1 = -2 + 4\n" then ()

 else raise error "auto-inform.sml: diff.behav.replaceFormula: on Frm 1 + = 1";

 autoCalculate 1 CompleteCalc;

 val ((pt,pos as(p,_)),_) = get_calc 1;

 if pos=([],Res)andalso"[x = 1]"=(term2str o fst)(get_obj g_result pt p)then()

 else raise error "auto-inform.sml: diff.behav.replaceFormula: on Frm 1 + = 2";

"--------- replaceFormula: cut calculation -----------------------";

"--------- replaceFormula: cut calculation -----------------------";

"--------- replaceFormula: cut calculation -----------------------";

 states:=[];

 CalcTree [(["equality (x+1=2)", "solveFor x","solutions L"], 

	    ("Test.thy", 

	     ["sqroot-test","univariate","equation","test"],

	     ["Test","squ-equ-test-subpbl1"]))];

 Iterator 1; moveActiveRoot 1;

 autoCalculate 1 CompleteCalc;

 moveActiveRoot 1; moveActiveDown 1;

 if get_pos 1 1 = ([1], Frm) then ()

 else raise error "auto-inform.sml: diff.behav. cut calculation 1";

 replaceFormula 1 "x + 1 = 4 + -2"; refFormula 1 (get_pos 1 1);

 val ((pt,p),_) = get_calc 1;

 val str = pr_ptree pr_short pt;

 writeln str;

 if p = ([1], Res) then ()

 else raise error "auto-inform.sml: diff.behav. cut calculation 2";

(* 040307 copied from informtest.sml; ... old version 

 "---------------- maximum-example, UC: Modeling / modifyCalcHead -";

 "---------------- maximum-example, UC: Modeling / modifyCalcHead -";

 "---------------- maximum-example, UC: Modeling / modifyCalcHead -";

 val p = ([],Pbl);

 val elems = ["fixedValues [r=Arbfix]","maximum A","valuesFor [a,b]",

	      "relations [A=a*b, (a/2)^^^2 + (b/2)^^^2 = r^^^2]",

	      "relations [A=a*b, (a/2)^^^2 + (b/2)^^^2 = r^^^2]",

	      "relations [A=a*b, a/2=r*sin alpha, b/2=r*cos alpha]",

	      (*^^^ these are the elements for the root-problem (in variants)*)

              (*vvv these are elements required for subproblems*)

	      "boundVariable a","boundVariable b","boundVariable alpha",

	      "interval {x::real. 0 <= x & x <= 2*r}",

	      "interval {x::real. 0 <= x & x <= 2*r}",

	      "interval {x::real. 0 <= x & x <= pi}",

	      "errorBound (eps=(0::real))"]

 (*specifying is not interesting for this example*)

 val spec = ("DiffApp.thy", ["maximum_of","function"], 

	     ["DiffApp","max_by_calculus"]);

 (*the empty model with descriptions for user-guidance by Model_Problem*)

 val empty_model = [Given ["fixedValues []"],

		    Find ["maximum", "valuesFor"],

		    Relate ["relations []"]];

 (*!!!!!!!!!!!!!!!!! DON'T USE me FOR FINDING nxt !!!!!!!!!!!!!!!!!!*)

 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(elems, spec)];

 (*val nxt = ("Model_Problem", ...*)

 val pbl = get_obj g_pbl pt (fst p); (writeln o (itms2str thy)) pbl; 

 val (p,_,f,nxt,_,pt) = me nxt p c pt;

 (*nxt = Add_Given "fixedValues [r = Arbfix]"*)

 val pbl = get_obj g_pbl pt (fst p); (writeln o (itms2str thy)) pbl; 

(*[

(0 ,[] ,false ,#Given ,Inc fixedValues [] ,(??.empty, [])),

(0 ,[] ,false ,#Find ,Inc maximum ,(??.empty, [])),

(0 ,[] ,false ,#Find ,Inc valuesFor ,(??.empty, [])),

(0 ,[] ,false ,#Relate ,Inc relations [] ,(??.empty, []))]*)

 (*the empty CalcHead is checked w.r.t the model and re-established as such*)

 val (b,pt,ocalhd) = input_icalhd pt (p,"", empty_model, Pbl, e_spec);

 val pbl = get_obj g_pbl pt (fst p); (writeln o (itms2str thy)) pbl; 

 if ocalhd2str ocalhd = "(Pbl, ??.empty, [\n(0 ,[] ,false ,#Given ,Inc fixedValues [] ,(??.empty, [])),\n(0 ,[] ,false ,#Find ,Inc maximum ,(??.empty, [])),\n(0 ,[] ,false ,#Find ,Inc valuesFor ,(??.empty, [])),\n(0 ,[] ,false ,#Relate ,Inc relations [] ,(??.empty, []))], [], \n(\"e_domID\", [\"e_pblID\"], [\"e_metID\"]) )" then () else raise error "informtest.sml: diff.behav. max 1";

 (*there is one input to the model (could be more)*)

 val (b,pt,ocalhd) = 

     input_icalhd pt (p,"", [Given ["fixedValues [r=Arbfix]"],

			     Find ["maximum", "valuesFor"],

			     Relate ["relations"]], Pbl, e_spec);

 val pbl = get_obj g_pbl pt (fst p); (writeln o (itms2str thy)) pbl; 

 if ocalhd2str ocalhd = "(Pbl, ??.empty, [\n(1 ,[1,2,3] ,true ,#Given ,Cor fixedValues [r = Arbfix] ,(fix_, [[r = Arbfix]])),\n(0 ,[] ,false ,#Find ,Inc maximum ,(??.empty, [])),\n(0 ,[] ,false ,#Find ,Inc valuesFor ,(??.empty, [])),\n(0 ,[] ,false ,#Relate ,Inc relations [] ,(??.empty, []))], [], \n(\"e_domID\", [\"e_pblID\"], [\"e_metID\"]) )" then () 

 else raise error "informtest.sml: diff.behav. max 2";

 (*this input is complete in variant 3, but the ME doesn't recognize FIXXXXME

 val (b,pt''''',ocalhd) = 

     input_icalhd pt (p,"", [Given ["fixedValues [r=Arbfix]"],

			     Find ["maximum A", "valuesFor [a,b]"],

			     Relate ["relations [A=a*b, a/2=r*sin alpha, \

				     \b/2=r*cos alpha]"]], Pbl, e_spec);

 val pbl = get_obj g_pbl pt''''' (fst p); (writeln o (itms2str thy)) pbl; 

 if ocalhd2str ocalhd = ------------^^^^^^^^^^ missing GOON !!!*)

 (*this input is complete in variant 1 (variant 3 does not work yet)*)

 val (b,pt''''',ocalhd) = 

     input_icalhd pt (p,"", [Given ["fixedValues [r=Arbfix]"],

			     Find ["maximum A", "valuesFor [a,b]"],

			     Relate ["relations [A=a*b, \

				     \(a/2)^^^2 + (b/2)^^^2 = r^^^2]"]], 

		      Pbl, e_spec);

 val pbl = get_obj g_pbl pt''''' (fst p); (writeln o (itms2str thy)) pbl; 

 modifycalcheadOK2xml 111 (bool2str b) ocalhd;

*)