(* use"../systest/scriptnew.sml";

   use"systest/scriptnew.sml";

   use"scriptnew.sml";

   *)

(*contents*)

" --- test 30.4.02 Testterm:  Repeat Repeat Or ------------------ ";

" --- test  9.5.02 Testeq: While Try Repeat @@ ------------------ ";

" --- test 11.5.02 Testeq: let e_e =... in [e_] ------------------ ";

" _________________ me + nxt_step from script ___________________ ";

" _________________ me + sqrt-equ-test: 1.norm_equation  ________ ";

" _________________ equation with x =(-12)/5, but L ={} ------- ";

"------------------ script with Map, Subst (biquadr.equ.)---------";

(*contents*)

"  --- test 30.4.02 Testterm:  Repeat Repeat Or ------------------ ";

"  --- test 30.4.02 Testterm:  Repeat Repeat Or ------------------ ";

"  --- test 30.4.02 Testterm:  Repeat Repeat Or ------------------ ";

store_pbt

 (prep_pbt Test.thy "pbl_testss" [] e_pblID

 (["tests"],

  []:(string * string list) list,

  e_rls, NONE, []));

store_pbt

 (prep_pbt Test.thy "pbl_testss_term" [] e_pblID

 (["met_testterm","tests"],

  [("#Given" ,["realTestGiven g_"]),

   ("#Find"  ,["realTestFind f_"])

  ],

  e_rls, NONE, []));

store_met

 (prep_met Test.thy "met_test_simp" [] e_metID

 (*test for simplification*)

 (["Test","met_testterm"]:metID,

  [("#Given" ,["realTestGiven g_"]),

   ("#Find"  ,["realTestFind f_"])

   ],

   {rew_ord'="tless_true",rls'=tval_rls,srls=e_rls,prls=e_rls,calc=[],

    crls=tval_rls, nrls=e_rls(*,

    asm_rls=[],asm_thm=[]*)},

 "Script Testterm (g_::real) =   \

 \Repeat\

 \  ((Repeat (Rewrite rmult_1 False)) Or\

 \   (Repeat (Rewrite rmult_0 False)) Or\

 \   (Repeat (Rewrite radd_0 False))) g_"

 ));

val fmz = ["realTestGiven ((0+0)*(1*(1*a)))","realTestFind F"];

val (dI',pI',mI') = ("Test.thy",["met_testterm","tests"],

		     ["Test","met_testterm"]);

(*val p = e_pos'; val c = []; 

val nxt = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));

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

val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];

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;

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

(*val nxt = ("Apply_Method",Apply_Method ("Test.thy","met_testterm"))*)

(*----script 111 ------------------------------------------------*)

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

(*"(#0 + #0) * (#1 * (#1 * a))"  nxt= Rewrite ("rmult_1",*)

(*----script 222 ------------------------------------------------*)

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

(*"(#0 + #0) * (#1 * a)"         nxt= Rewrite ("rmult_1",*)

(*----script 333 ------------------------------------------------*)

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

(*"(#0 + #0) * a"                nxt= Rewrite ("radd_0",*)

(*----script 444 ------------------------------------------------*)

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

(*"#0 * a"*)

(*----script 555 ------------------------------------------------*)

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

(*"#0"*)

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

else error ("new behaviour in 30.4.02 Testterm: p="^(pos'2str p));

(*----script 666 ------------------------------------------------*)

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

(*"#0"*)

if nxt=("End_Proof'",End_Proof') then ()

else error "new behaviour in 30.4.02 Testterm: End_Proof";

"  --- test 9.5.02 Testeq: While Try Repeat @@ ------------------ ";

"  --- test 9.5.02 Testeq: While Try Repeat @@ ------------------ ";

"  --- test 9.5.02 Testeq: While Try Repeat @@ ------------------ ";

store_pbt

 (prep_pbt Test.thy "pbl_testss_eq" [] e_pblID

 (["met_testeq","tests"],

  [("#Given" ,["boolTestGiven e_e"]),

   ("#Find"  ,["boolTestFind v_i_"])

  ],

  e_rls, NONE, []));

store_met

 (prep_met Test.thy "met_test_eq1" [] e_metID

 (["Test","testeq1"]:metID,

   [("#Given",["boolTestGiven e_e"]),

   ("#Where" ,[]), 

   ("#Find"  ,["boolTestFind v_i_"]) 

   ],

   {rew_ord'="tless_true",rls'=tval_rls,

    srls=append_rls "testeq1_srls" e_rls 

		    [Calc ("Test.contains'_root", eval_contains_root"")],

    prls=e_rls,calc=[], crls=tval_rls, nrls=e_rls

		  (*,asm_rls=[],asm_thm=[("square_equation_left","")]*)},

 "Script Testeq (e_e::bool) =                                        \

   \(While (contains_root e_e) Do                                     \

   \((Try (Repeat (Rewrite rroot_square_inv False))) @@    \

   \  (Try (Repeat (Rewrite square_equation_left True))) @@ \

   \  (Try (Repeat (Rewrite radd_0 False)))))\

   \ e_e"

 ));

val fmz = ["boolTestGiven (0+(sqrt(sqrt(sqrt a))^^^2)^^^2=0)",

	   "boolTestFind v_i_"];

val (dI',pI',mI') = ("Test.thy",["met_testeq","tests"],

		     ["Test","testeq1"]);

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

atomt sc;

(*val p = e_pos'; val c = []; 

val nxt = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));

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

val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];

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;

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

(*val nxt = ("Apply_Method",Apply_Method ("Test.thy","testeq1")) *)

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 f = Form' (FormKF (~1,EdUndef,1,Nundef,"#0 + sqrt a = #0"))

val nxt = ("Rewrite",Rewrite ("radd_0","#0 + ?k = ?k"))*)

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

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

(*** No such constant: "Test.contains'_root"  *)

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

if f=(Form' (FormKF (~1,EdUndef,0,Nundef,"a = 0 ^^^ 2"))) andalso

   nxt=("End_Proof'",End_Proof') then ()

else error "different behaviour test 9.5.02 Testeq: While Try Repeat @@";

" --- test 11.5.02 Testeq: let e_e =... in [e_] --------- ";

" --- test 11.5.02 Testeq: let e_e =... in [e_] --------- ";

" --- test 11.5.02 Testeq: let e_e =... in [e_] --------- ";

store_met

 (prep_met Test.thy "met_test_let" [] e_metID

 (["Test","testlet"]:metID,

   [("#Given",["boolTestGiven e_e"]),

   ("#Where" ,[]), 

   ("#Find"  ,["boolTestFind v_i_"]) 

   ],

   {rew_ord'="tless_true",rls'=tval_rls,

    srls=append_rls "testlet_srls" e_rls 

		    [Calc ("Test.contains'_root",eval_contains_root"")],

    prls=e_rls,calc=[], crls=tval_rls, nrls=e_rls

		  (*,asm_rls=[],asm_thm=[("square_equation_left","")]*)},

   "Script Testeq2 (e_e::bool) =                                        \

   \(let e_e =\

   \  ((While (contains_root e_e) Do                                     \

   \   (Rewrite square_equation_left True))\

   \   e_e)\

   \in [e_::bool])"

   ));

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

writeln(term2str sc);

val fmz = ["boolTestGiven (sqrt a = 0)",

	   "boolTestFind v_i_"];

val (dI',pI',mI') = ("Test.thy",["met_testeq","tests"],

		     ["Test","testlet"]);

(*val p = e_pos'; val c = []; 

val nxt = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));

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

val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];

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;

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

(*val nxt = ("Apply_Method",Apply_Method ("Test.thy","testlet"))*)

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;

if f=(Form' (FormKF (~1,EdUndef,0,Nundef,"[a = 0 ^^^ 2]"))) andalso

   nxt=("End_Proof'",End_Proof') then ()

else error "different behaviour in test 11.5.02 Testeq: let e_e =... in [e_]";

" _________________ me + nxt_step from script _________________ ";

" _________________ me + nxt_step from script _________________ ";

" _________________ me + nxt_step from script _________________ ";

val fmz = ["equality (sqrt(9+4*x)=sqrt x + sqrt(5+x))",

	   "solveFor x","solutions L"];

val (dI',pI',mI') =

  ("Test.thy",["sqroot-test","univariate","equation","test"],

   ["Test","sqrt-equ-test"]);

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

writeln(term2str sc);

"--- s1 ---";

(*val p = e_pos'; val c = []; 

val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));

val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)

val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];

"--- s2 ---";

val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

(* val nxt =

  ("Add_Given",

   Add_Given "equality (sqrt (#9 + #4 * x) = sqrt x + sqrt (#5 + x))");*)

val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

"--- s3 ---";

(* val nxt = ("Add_Given",Add_Given "solveFor x");*)

val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

"--- s4 ---";

(* val nxt = ("Add_Given",Add_Given "errorBound (eps = #0)");*)

"--- s5 ---";

(* val nxt = ("Add_Find",Add_Find "solutions L");*)

val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

"--- s6 ---";

(* val nxt = ("Specify_Theory",Specify_Theory "Test.thy");*)

val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

"--- s7 ---";

(* val nxt =

  ("Specify_Problem",

   Specify_Problem ["sqroot-test","univariate","equation","test"]);*)

val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

"--- s8 ---";

(* val nxt = ("Specify_Method",Specify_Method ("Test.thy","sqrt-equ-test"));*)

val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

"--- s9 ---";

(* val nxt = ("Apply_Method",Apply_Method ("Test.thy","sqrt-equ-test"));*)

val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

"--- 1 ---";

(* val nxt = ("Rewrite",Rewrite ("square_equation_left",""));*)

val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

"--- 2 ---";

(* val nxt = ("Rewrite_Set",Rewrite_Set "Test_simplify");*)

val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

"--- 3 ---";

(* val nxt = ("Rewrite_Set",Rewrite_Set "rearrange_assoc");*)

val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

"--- 4 ---";

(* val nxt = ("Rewrite_Set",Rewrite_Set "isolate_root");*)

val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

"--- 5 ---";

(* val nxt = ("Rewrite_Set",Rewrite_Set "Test_simplify");*)

val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

"--- 6 ---";

(* val nxt = ("Rewrite",Rewrite ("square_equation_left",""));*)

val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

"--- 7 ---";

(* val nxt = ("Rewrite_Set",Rewrite_Set "Test_simplify");*)

val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

"--- 8<> ---";

(* val nxt = ("Rewrite_Set",Rewrite_Set "rearrange_assoc");*)

val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

"--- 9<> ---";

(* val nxt = ("Rewrite_Set",Rewrite_Set "Test_simplify");*)

val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

"--- 10<> ---";

(* val nxt = ("Rewrite_Set",Rewrite_Set "norm_equation");*)

val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

"--- 11<> ---";

(* val nxt = ("Rewrite_Set",Rewrite_Set "Test_simplify");*)

val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

"--- 12<> ---.";

(* val nxt = ("Rewrite_Set_Inst",Rewrite_Set_Inst (["(bdv,x)"],"isolate_bdv"));*)

val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

"--- 13<> ---";

(* val nxt = ("Rewrite_Set",Rewrite_Set "Test_simplify");*)

val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

"--- 14<> ---";

(* nxt = ("Check_Postcond",Check_Postcond ("Test.thy","sqrt-equ-test"));*)

val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

if f<>(Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 4]")))

then error "scriptnew.sml 1: me + tacs from script: new behaviour" 

else ();

"--- 15<> ---";

(* val nxt = ("End_Proof'",End_Proof');*)

val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

writeln (pr_ptree pr_short pt);

writeln("result: "^((term2str o fst o (get_obj g_result pt)) [])^

"\n=============================================================");

(*get_obj g_asm pt [];

val it = [("#0 <= sqrt x + sqrt (#5 + x)",[1]),("#0 <= #9 + #4 * x",[1]),...*)

" _________________ me + sqrt-equ-test: 1.norm_equation  _________________ ";

" _________________ me + sqrt-equ-test: 1.norm_equation  _________________ ";

" _________________ me + sqrt-equ-test: 1.norm_equation  _________________ ";

val fmz = ["equality (sqrt(9+4*x)=sqrt x + sqrt(5+x))",

	   "solveFor x","errorBound (eps=0)",

	   "solutions L"];

val (dI',pI',mI') =

  ("Test.thy",["sqroot-test","univariate","equation","test"],

   ["Test","sqrt-equ-test"]);

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

 (writeln o term2str) sc;

"--- s1 ---";

(*val p = e_pos'; val c = []; 

val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));

val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)

val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];

"--- s2 ---";

val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

(* val nxt = ("Add_Given",

   Add_Given "equality (sqrt (#9 + #4 * x) = sqrt x + sqrt (#5 + x))");*)

val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

"--- s3 ---";

(* val nxt = ("Add_Given",Add_Given "solveFor x");*)

val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

"--- s4 ---";

(* val nxt = ("Add_Given",Add_Given "errorBound (eps = #0)");*)

(*val (p,_,f,nxt,_,pt) = me nxt p [1] pt;*)

"--- s5 ---";

(* val nxt = ("Add_Find",Add_Find "solutions L");*)

val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

"--- s6 ---";

(* val nxt = ("Specify_Theory",Specify_Theory "Test.thy");*)

val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

"--- s7 ---";

(* val nxt = ("Specify_Problem",

   Specify_Problem ["sqroot-test","univariate","equation","test"]);*)

val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

"--- s8 ---";

(* val nxt = ("Specify_Method",Specify_Method ("Test.thy","sqrt-equ-test"));*)

val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

"--- s9 ---";

(* val nxt = ("Apply_Method",Apply_Method ("Test.thy","sqrt-equ-test"));*)

val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

(*"sqrt (9 + 4 * x) = sqrt x + sqrt (5 + x)"*)

"--- !!! x1 --- 1.norm_equation";

(*###*)val nxt = ("Rewrite_Set",Rewrite_Set "norm_equation");

val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

"--- !!! x2 --- 1.norm_equation";

(*meNEW: "9 + 4 * x = (sqrt x + sqrt (5 + x)) ^^^ 2" -- NICHT norm_equation!!*)

(*meOLD: "sqrt (9 + 4 * x) + -1 * (sqrt x + sqrt (5 + x)) = 0"*)

(* val nxt = ("Rewrite_Set",Rewrite_Set "Test_simplify");*)

val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

(*"-1 * sqrt x + (-1 * sqrt (5 + x) + sqrt (9 + 4 * x)) = 0"*)

(*(me nxt p [1] pt) handle e => print_exn_G e;*)

"--- !!! x3 --- 1.norm_equation";

(*val nxt = ("Empty_Tac",Empty_Tac) ### helpless*)

(*###*)val nxt = ("Rewrite_Set",Rewrite_Set "rearrange_assoc");

val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

"--- !!! x4 --- 1.norm_equation";

(*"-1 * sqrt x + -1 * sqrt (5 + x) + sqrt (9 + 4 * x) = 0"*)

(*val nxt = ("Rewrite_Set",Rewrite_Set "isolate_root")*)

val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

"--- !!! x5 --- 1.norm_equation";

(*"sqrt (9 + 4 * x) = 0 + -1 * (-1 * sqrt x + -1 * sqrt (5 + x))"*)

(* val nxt = ("Rewrite_Set",Rewrite_Set "Test_simplify");*)

val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

(*FIXXXXXXXXXXXXXXXXXXXXXXXME reestablish check:

if f= Form'(FormKF(~1,EdUndef,1,Nundef,"sqrt (9 + 4 * x) = sqrt x + sqrt (5 + x)"))

then() else error "new behaviour in test-example 1.norm sqrt-equ-test";

#################################################*)

(* use"../tests/scriptnew.sml";

   *)

" _________________ equation with x =(-12)/5, but L ={} ------- ";

val fmz = ["equality (sqrt(9+4*x)=sqrt x + sqrt(-3+x))",

	   "solveFor x","errorBound (eps=0)",

	   "solutions L"];

val (dI',pI',mI') =

  ("Test.thy",["sqroot-test","univariate","equation","test"],

   ["Test","square_equation"]);

(*val p = e_pos'; val c = []; 

val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));

val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)

val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];

val (p,_,f,nxt,_,pt) = me nxt p [1] 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;

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

(*val nxt = ("Apply_Method",Apply_Method ["Test","square_equation"])*)

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

(*val nxt = "square_equation_left",

      "[| 0 <= ?a; 0 <= ?b |] ==> (sqrt ?a = ?b) = (?a = ?b ^^^ 2)"))*)

get_assumptions_ pt p;

(*it = [] : string list;*)

trace_rewrite:=true;

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

trace_rewrite:=false;

val asms = get_assumptions_ pt p;

if asms = [(str2term "0 <= 9 + 4 * x",[1]),

	   (str2term "0 <= x",[1]),

	   (str2term "0 <= -3 + x",[1])] then ()

else error "scriptnew.sml diff.behav. in sqrt assumptions 1";

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 nxt = Rewrite ("square_equation_left",     *)

val asms = get_assumptions_ pt p;

[("0 <= 9 + 4 * x",[1]),("0 <= x",[1]),("0 <= -3 + x",[1])];

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

val asms = get_assumptions_ pt p;

if asms = [(str2term "0 <= 9 + 4 * x",[1]),

	   (str2term "0 <= x",[1]),

	   (str2term "0 <= -3 + x",[1]),

	   (str2term "0 <= x ^^^ 2 + -3 * x",[6]),

	   (str2term "0 <= 6 + x",[6])] then ()

else error "scriptnew.sml diff.behav. in sqrt assumptions 2";

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;

(*val nxt = Subproblem ("Test.thy",["linear","univariate","equation","test"*)

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;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 nxt = ("Apply_Method",Apply_Method ["Test","solve_linear"])*)

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 nxt =

  ("Check_Postcond",Check_Postcond ["linear","univariate","equation","test"])*)

val asms = get_assumptions_ pt p;

if asms = [] then ()

else error "scriptnew.sml diff.behav. in sqrt assumptions 3";

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

(*val nxt = ("Check_elementwise",Check_elementwise "Assumptions")*)

val asms = get_assumptions_ pt p;

if asms = [(str2term "0 <= 9 + 4 * x",[1]),

	   (str2term "0 <= x",[1]),

	   (str2term "0 <= -3 + x",[1]),

	   (str2term "0 <= x ^^^ 2 + -3 * x",[6]),

	   (str2term "0 <= 6 + x",[6])] then ()

else raise 

    error "scriptnew.sml: diff.behav. at Check_elementwise [x = -12 / 5]";

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

(*val nxt = Check_Postcond ["sqroot-test","univariate","equation","test"])*)

val asms = get_assumptions_ pt p;

[("0 <= 9 + 4 * x",[1]),("0 <= x",[1]),("0 <= -3 + x",[1]),

   ("0 <= x ^^^ 2 + -3 * x",[6]),("0 <= 6 + x",[6]),

   ("0 <= 6 + -12 / 5 &\n0 <= (-12 / 5) ^^^ 2 + -3 * (-12 / 5) &\n0 <= -3 + -12 / 5 & 0 <= -12 / 5 & 0 <= 9 + 4 * (-12 / 5)",

    [13])];

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

val Form' (FormKF (_,_,_,_,ff)) = f;

if ff="[x = -12 / 5]"

then writeln("there should be L = []\nthere should be L = []\nthere should be L = []\nthere should be L = []\nthere should be L = []\n")

else error "diff.behav. in scriptnew.sml; root-eq: L = []";

val asms = get_assumptions_ pt p;

if asms = [(str2term "0 <= 9 + 4 * (-12 / 5)",[]),

	   (str2term "0 <= -12 / 5", []),

	   (str2term "0 <= -3 + -12 / 5", []),

	   (str2term "0 <= (-12 / 5) ^^^ 2 + -3 * (-12 / 5)", []),

	   (str2term "0 <= 6 + -12 / 5", [])] then ()

else error "scriptnew.sml diff.behav. in sqrt assumptions 4";

"------------------ script with Map, Subst (biquadr.equ.)---------";

"------------------ script with Map, Subst (biquadr.equ.)---------";

"------------------ script with Map, Subst (biquadr.equ.)---------";

(*GoOn.5.03. script with Map, Subst (biquadr.equ.)

val scr = Script (((inst_abs thy) o term_of o the o (parse thy))

    "Script Biquadrat_poly (e_e::bool) (v_::real) =                       \

    \(let e_e = Substitute [(v_^^^4, v_0_^^^2),(v_^^^2, v_0_)] e_;        \ 

    \     L_0_ = (SubProblem (PolyEq_,[univariate,equation], [no_met])   \

    \             [BOOL e_e, REAL v_0_]);                               \ 

    \     L_i_ = Map (((Substitute [(v_0_, v_^^^2)]) @@                  \

    \                  ((Rewrite real_root_positive False) Or            \

    \                   (Rewrite real_root_negative False)) @@           \

    \                  OrToList) L_0_                                    \ 

    \ in (flat ....))"

);

*)