(* use"systest/subp-rooteq.sml";

   use"subp-rooteq.sml";

   *)

val c = [];

"---------------- miniscript with mini-subpbl -------------";

"---------------- solve_linear as rootpbl -----------------";

"---------------- solve_plain_square as rootpbl -----------";

"---------------- root-eq + subpbl: solve_linear ----------";

"---------------- root-eq + subpbl: solve_plain_square ----";

"---------------- root-eq + subpbl: no_met: linear --------";

"---------------- root-eq + subpbl: no_met: square --------";

"---------------- no_met in rootpbl -> linear -------------";

"==========================================================";

"---------------- miniscript with mini-subpbl -------------";

"---------------- miniscript with mini-subpbl -------------";

"---------------- miniscript with mini-subpbl -------------";

(*###########################################################

  ##  12.03 next_tac repariert (gab keine Value zurueck   ###

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

val fmz = ["equality (x+1=(2::real))", "solveFor x","solutions L"];

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

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

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

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

(writeln o term2str) sc;

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 [1] pt;

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

(*val nxt = ("Add_Find",Add_Find "solutions L") : string * tac*)

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

(*val nxt = ("Specify_Theory",Specify_Theory "Test") : string * tac*)

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

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

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

(*("Specify_Method",Specify_Method ("Test","squ-equ-test-subpbl1"))*)

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

(*val nxt = ("Apply_Method",Apply_Method ("Test","squ-equ-test-subpbl1"*)

(*---vvv--- nxt_ here = loc_ below ------------------vvv-------------------*)

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

(*val f = "x + 1 = 2"; val nxt = Rewrite_Set "norm_equation"*)

(*### solve Apply_Method: is =   ### nxt_solv1 Apply_Method: store is

ScrState (["

(e_, x + 1 = 2)","

(v_, x)"],

 [], NONE,

 ??.empty, Safe, true)           ########## OK*)

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

(*val f = "x + 1 + -1 * 2 = 0"; val nxt = Rewrite_Set "Test_simplify"*)

(*### locate_gen----------: is=  ### next_tac----------------:E =

ScrState (["

(e_, x + 1 = 2)","

(v_, x)"],

 [], NONE,

 ??.empty, Safe, true)           ########## OK von loc_ uebernommen

### solve, after locate_gen: is= ### nxt_solv4 Apply_Method: stored is =

ScrState (["

(e_, x + 1 = 2)","

(v_, x)"],

 [R,L,R,L,L,R,R], SOME e_e,

 x + 1 + -1 * 2 = 0, Safe, true) ########## OK*)

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

(*val f = "-1 + x = 0"; val nxt = Subproblem ("Test",[#,#,#])

                                ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~*)

(*### locate_gen-----------: is= ### next_tac-----------------: E=

ScrState (["

(e_, x + 1 = 2)","

(v_, x)"],

 [R,L,R,L,L,R,R], SOME e_e,

 x + 1 + -1 * 2 = 0, Safe, true) ########## OK von loc_ uebernommen

### solve, after locate_gen: is= ### nxt_solv4 Apply_Method: stored is =

ScrState (["

(e_, x + 1 = 2)","

(v_, x)"],

 [R,L,R,L,R,R], SOME e_e,

 -1 + x = 0, Safe, false)         ########## OK*)

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

(*### locate_gen------------: is= ### next_tac-----------------: E=

ScrState (["

(e_, x + 1 = 2)","

(v_, x)"],

 [R,L,R,L,R,R], SOME e_e,

 -1 + x = 0, Safe, false)         ########## OK von loc_ uebernommen

### solve, after locate_gen: is=  ### nxt_solv4 Apply_Method: stored is =

ScrState (["

(e_, -1 + x = 0)","

(v_, x)"],

 [R,R,D,L,R], SOME e_e,

 Subproblem (Test.thy, [linear, univariate, equation, test]), Safe, true)

                                  ########## OK*)

  p;

  writeln(istate2str (fst (get_istate pt ([3],Frm))));

(*val nxt = ("Model_Problem",Model_Problem ["LINEAR","univariate","equation"]*)

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

(*val nxt = ("Add_Given",Add_Given "equality (-1 + x = 0)") *)

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

(*val nxt = ("Add_Given",Add_Given "solveFor x") : string * tac*)

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

(*val nxt = ("Add_Find",Add_Find "solutions x_i") : string * tac*)

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

(*val nxt = ("Specify_Theory",Specify_Theory "Test")*)

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

(*("Specify_Problem",Specify_Problem ["LINEAR","univariate","equation"])*)

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

(*val nxt = ("Specify_Method",Specify_Method ("Test","solve_linear"))*)

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

  (writeln o term2str) sc;

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

(*val nxt = ("Apply_Method",Apply_Method ("Test","solve_linear"))*)

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

(*val nxt = ("Rewrite_Set_Inst",Rewrite_Set_Inst ([#],"isolate_bdv"))*)

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

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

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

(*val nxt = ("Check_Postcond",Check_Postcond ["LINEAR","univariate","eq*)

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

  p;

  writeln(istate2str (fst (get_istate pt ([3],Res))));

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

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

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

val Form' (FormKF (_,EdUndef,0,Nundef,res)) = f;

if (snd nxt)=End_Proof' andalso res="[x = 1]" then ()

else error "subp-rooteq.sml: new.behav. in  miniscript with mini-subpbl";

"---------------- solve_linear as rootpbl -----------------";

"---------------- solve_linear as rootpbl -----------------";

"---------------- solve_linear as rootpbl -----------------";

val fmz = ["equality (1+-1*2+x=(0::real))",

	   "solveFor x","solutions L"];

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

  ("Test",["LINEAR","univariate","equation","test"],

   ["Test","solve_linear"]);

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

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

(*val nxt = ("Add_Given",Add_Given "equality (x + #1 + #-1 * #2 = #0)")*)

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

(*val nxt = ("Add_Given",Add_Given "solveFor x") : string * tac*)

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

(*val nxt = ("Add_Find",Add_Find "solutions L") : string * tac*)

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

(*val nxt = ("Specify_Theory",Specify_Theory "Test") : string * tac*)

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

(*val nxt = ("Specify_Problem",Specify_Problem ["univariate","equation"])*)

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

(*val nxt = ("Specify_Method",Specify_Method ("Test","solve_linear"))*)

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

(*val nxt = ("Apply_Method",Apply_Method ("Test","solve_linear"))*)

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

(*val f = Form' (FormKF (~1,EdUndef,1,Nundef,"#1 + #-1 * #2 + x = #0"))

  val nxt = ("Rewrite_Set_Inst",Rewrite_Set_Inst ([#],"isolate_bdv"))*)

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

(*val f = Form' (FormKF (~1,EdUndef,1,Nundef,"x = #0 + #-1 * (#1 + #-1 * #2)"))

  val nxt = ("Rewrite_Set",Rewrite_Set "Test_simplify") : string * tac*)

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

(*val f = Form' (FormKF (~1,EdUndef,1,Nundef,"x = #1")) : mout                   val nxt = ("Check_Postcond",Check_Postcond ["univariate","equation"])*)

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

(*val f = Form' (FormKF (~1,EdUndef,0,Nundef,"[x = #1]")) : mout 

  val nxt = ("End_Proof'",End_Proof') : string * tac*)

val Form' (FormKF (_,EdUndef,0,Nundef,res)) = f;

if (snd nxt)=End_Proof' andalso res="[x = 1]" then ()

else error "subp-rooteq.sml: new.behav. in  solve_linear as rootpbl";

"---------------- solve_plain_square as rootpbl -----------";

"---------------- solve_plain_square as rootpbl -----------";

"---------------- solve_plain_square as rootpbl -----------";

val fmz = ["equality (9 + -1 * x ^^^ 2 = 0)","solveFor x",

	   "solutions L"];

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

  ("Test",["plain_square","univariate","equation","test"],

   ["Test","solve_plain_square"]);

(*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 [1] pt;

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

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

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

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

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

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

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

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

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

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

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

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

val  Form' (FormKF (~1,EdUndef,0,Nundef,res)) = f;

if snd nxt=End_Proof' andalso res="[x = -3, x = 3]" then ()

else error "subp-rooteq.sml: new.behav. in  solve_plain_square as rootpbl";

"---------------- root-eq + subpbl: solve_linear ----------";

"---------------- root-eq + subpbl: solve_linear ----------";

"---------------- root-eq + subpbl: solve_linear ----------";

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

	   "solveFor x","solutions L"];

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

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

   ["Test","square_equation1"]);

(*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 [1] pt;

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

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

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

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

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

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

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

square_equation_left*)

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

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

Test_simplify*)

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

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

rearrange_assoc*)

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

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

isolate_root*)

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

(*"sqrt (x ^^^ 2 + 5 * x) = (5 + 2 * x + -1 * (9 + 4 * x)) / (-1 * 2)"

Test_simplify*)

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

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

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

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

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

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

(*"x ^^^ 2 + 5 * x + -1 * (4 + (x ^^^ 2 + 4 * x)) = 0"*)

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

(*"-4 + x = 0"

  val nxt =("Subproblem",Subproblem ("Test",["LINEAR","univariate"...*)

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

(*val nxt =("Model_Problem",Model_Problem ["LINEAR","univariate"...*)

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

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

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

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

(*val nxt = ("Specify_Theory",Specify_Theory "Test")*)

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

(*("Specify_Problem",Specify_Problem ["LINEAR","univariate","equation"])*)

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

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

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

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

(*"x = 0 + -1 * -4", nxt Test_simplify*)

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

(*"x = 4", nxt Check_Postcond ["LINEAR","univariate","equation","test"]*)

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

(*"[x = 4]", nxt Check_elementwise "Assumptions"*)

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

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

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

val Form' (FormKF (~1,EdUndef,0,Nundef,res)) = f;

if (snd nxt)=End_Proof' andalso res="[x = 4]" then ()

else error "subp-rooteq.sml: new.behav. in  root-eq + subpbl: solve_linear";

"---------------- root-eq + subpbl: solve_plain_square ----";

"---------------- root-eq + subpbl: solve_plain_square ----";

"---------------- root-eq + subpbl: solve_plain_square ----";

val fmz = ["equality (sqrt(5+x)+sqrt(5-x)=sqrt 18)",

	   "solveFor x","solutions L"];

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

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

   ["Test","square_equation2"]);

val Prog sc = (#scr o get_met) ["Test","square_equation2"];

(writeln o term2str) sc;

(*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 [1] pt;

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

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

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

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

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

(*val nxt = ("Apply_Method",Apply_Method ("Test","square_equation1"))*)

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

me nxt p [1] pt;

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

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

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

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

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

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

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

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

(*"9 + -1 * x ^^^ 2 = 0"

  Subproblem ("Test",["plain_square","univariate","equation"]))*)

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

(*Model_Problem ["plain_square","univariate","equation"]*)

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

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

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

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

(*val nxt = ("Specify_Theory",Specify_Theory "Test")*)

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

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

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

(*Apply_Method ("Test","solve_plain_square")*)

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

(*"9 + -1 * x ^^^ 2 = 0", nxt Rewrite_Set "isolate_bdv"*)

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

(*"x ^^^ 2 = (0 + -1 * 9) / -1", nxt Rewrite_Set "Test_simplify"*)

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

(*"x ^^^ 2 = 9", nxt Rewrite ("square_equality"*)

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

(*"x = sqrt 9 | x = -1 * sqrt 9", nxt Rewrite_Set "tval_rls"*)

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

(*"x = -3 | x = 3", nxt Or_to_List*)

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

(*"[x = -3, x = 3]", 

  nxt Check_Postcond ["plain_square","univariate","equation","test"]*)

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

(*"[x = -3, x = 3]", nxt Check_elementwise "Assumptions"*)

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

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

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

val Form' (FormKF (~1,EdUndef,0,Nundef,res)) = f;

if (snd nxt)=End_Proof' andalso res="[x = -3, x = 3]" then ()

else error "subp-rooteq.sml: new.behav. in  root-eq + subpbl: solve_plain_square";

writeln (pr_ctree pr_short pt);

val Prog s = (#scr o get_met) ["Test","square_equation"];

atomt s;

"---------------- root-eq + subpbl: no_met: linear ----";

"---------------- root-eq + subpbl: no_met: linear ----";

"---------------- root-eq + subpbl: no_met: linear ----";

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

	   "solveFor x","solutions L"];

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

  ("Test",["squareroot","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 [1] pt;

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

(*"-4 + x = 0", nxt Subproblem ("Test",["univariate","equation"]))*)

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

(*val nxt =("Model_Problem",Model_Problem ["LINEAR","univar...*)

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

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

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

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

(*val nxt = ("Specify_Theory",Specify_Theory "Test")*)

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

(*val nxt = ("Specify_Problem",Specify_Problem ["LINEAR","univariate","equ*)

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

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

(*Apply_Method ("Test","norm_univar_equation")*)

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

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

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

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

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

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

else error ("subp-rooteq.sml: new.behav. in  \

		 \root-eq + subpbl: solve_linear, p ="^(pos'2str p));

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

val Form' (FormKF (~1,EdUndef,0,Nundef,res)) = f;

if (snd nxt)=End_Proof' andalso res="[x = 4]" then ()

else error "subp-rooteq.sml: new.behav. in  root-eq + subpbl: solve_plain_square";

"---------------- root-eq + subpbl: no_met: square ----";

"---------------- root-eq + subpbl: no_met: square ----";

"---------------- root-eq + subpbl: no_met: square ----";

val fmz = ["equality (sqrt(5+x)+sqrt(5-x)=sqrt 18)",

	   "solveFor x","solutions L"];

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

  ("Test",["squareroot","univariate","equation","test"],

   ["Test","square_equation"]);

 val Prog sc = (#scr o get_met) ["Test","square_equation"];

 (writeln o term2str) sc;

(*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 [1] pt;

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

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

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

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

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

(*val nxt = ("Apply_Method",Apply_Method ("Test","square_equation1"))*)

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

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

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

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

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

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

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

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

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

(*Subproblem ("Test",["univariate","equation"]))*)

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

(*Model_Problem ["plain_square","univariate","equation"]*)

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

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

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

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

(*val nxt = ("Specify_Theory",Specify_Theory "Test")*)

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

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

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

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

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

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

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

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

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

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

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

(*val nxt = ("Check_Postcond",Check_Postcond ["squareroot","univariate","equ*)

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

val Form' (FormKF (~1,EdUndef,0,Nundef,res)) = f;

if (snd nxt)=End_Proof' andalso res="[x = -3, x = 3]" then ()

else error "subp-rooteq.sml: new.behav. in  root-eq + subpbl: no_met: square";

"---------------- no_met in rootpbl -> linear --------------";

"---------------- no_met in rootpbl -> linear --------------";

"---------------- no_met in rootpbl -> linear --------------";

val fmz = ["equality (1+2*x+3=4*x- 6)",

	   "solveFor x","solutions L"];

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

  ("Test",["univariate","equation","test"],

   ["no_met"]);

(*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 nxt = ("Model_Problem",Model_Problem ["normalize","univariate","equati*)

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","norm_univar_equation"*)

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",Subproblem ("Test",["univariate","equation"])*)

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

(*val nxt = ("Model_Problem",Model_Problem ["LINEAR","univariate","equation"]*)

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","equatio*)

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

(*val nxt = ("Check_Postcond",Check_Postcond ["normalize","univariate","equa*)

val (p,_,Form' (FormKF (_,_,_,_,f)),nxt,_,_) = 

    me nxt p c pt;

if f="[x = 5]" andalso nxt=("End_Proof'",End_Proof') then ()

else error "subp-rooteq.sml: new.behav. in no_met in rootpbl -> linear ---";

refine fmz ["univariate","equation","test"];

match_pbl fmz (get_pbt ["polynomial","univariate","equation","test"]);