(* tests for sml/ME/ctree.sml

   authors: Walther Neuper 060113

   (c) due to copyright terms

use"../smltest/ME/ctree.sml";

use"ctree.sml";

*)

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

"table of contents -----------------------------------------------";

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

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

"-------------- fun get_ctxt -------------------------------------";

"-------------- fun update_ctxt, fun g_ctxt ----------------------";

"-------------- check positions in miniscript --------------------";

"-------------- get_allpos' (from ptree above)--------------------";

"-------------- cut_level (from ptree above)----------------------";

"-------------- cut_tree (from ptree above)-----------------------";

"=====new ptree 1a miniscript with mini-subpbl ===================";

"-------------- cut_level ( ,Frm) on Incomplete Nd ---------------";

"=====new ptree 2 miniscript with mini-subpbl ====================";

"-------------- cut_tree (intermedi.ptree: 3rd level)-------------";

"-------------- cappend (from ptree above)------------------------";

"-------------- cappend minisubpbl -------------------------------";

"=====new ptree 3 ================================================";

"-------------- move_dn ------------------------------------------";

"-------------- move_dn: Frm -> Res ------------------------------";

"-------------- move_up ------------------------------------------";

"------ move into detail -----------------------------------------";

"=====new ptree 3a ===============================================";

"-------------- move_dn in Incomplete ctree ----------------------";

"=====new ptree 4: crooked by cut_level_'_ =======================";

(*############## development stopped 0501 ########################*)

(******************************************************************)

(*              val SAVE_get_trace = get_trace;                   *)

(******************************************************************)

"-------------- get_interval from ctree: incremental development--";

(******************************************************************)

(*              val get_trace = SAVE_get_trace;                   *)

(******************************************************************)

(*############## development stopped 0501 ########################*)

"=====new ptree 4 ratequation ====================================";

"-------------- pt_extract form, tac, asm<>[] --------------------";

"=====new ptree 5 minisubpbl =====================================";

"-------------- pt_extract form, tac, asm ------------------------";

"=====new ptree 6 minisubpbl intersteps ==========================";

"-------------- get_allpos' new ----------------------------------";

"-------------- cut_tree new (from ptree above)-------------------";

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

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

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

"-------------- fun get_ctxt -------------------------------------";

"-------------- fun get_ctxt -------------------------------------";

"-------------- fun get_ctxt -------------------------------------";

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 (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];

(get_ctxt pt p)

  handle _ => error "--- fun get_ctxt not even some ctxt found in PblObj";

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

(get_ctxt pt p)

  handle _ => error "--- fun get_ctxt not even some ctxt found in PrfObj";

"-------------- fun update_ctxt, fun g_ctxt ----------------------";

"-------------- fun update_ctxt, fun g_ctxt ----------------------";

"-------------- fun update_ctxt, fun g_ctxt ----------------------";

val pt = EmptyPtree;

val pt = append_problem [] (e_istate, e_ctxt) e_fmz ([(*oris*)], e_spec, e_term) pt;

val ctxt = get_obj g_ctxt pt [];

if is_e_ctxt ctxt then () else error "--- fun update_ctxt, fun g_ctxt: append_problem changed";

val pt = update_ctxt pt [] (ProofContext.init_global @{theory "Isac"});

if (get_obj g_ctxt pt [] |> ProofContext.theory_of |> Context.theory_name) = "Isac"

then () else error "--- fun update_ctxt, fun g_ctxt changed";

"-------------- check positions in miniscript --------------------";

"-------------- check positions in miniscript --------------------";

"-------------- check positions in miniscript --------------------";

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 (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];

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

(* nxt = Add_Given "equality (x + 1 = 2)"

   (writeln o (itms2str_ ctxt)) (get_obj g_pbl pt (fst p));

   *)

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

(* (writeln o (itms2str_ ctxt)) (get_obj g_pbl pt (fst p));

   *)

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

(* (writeln o (itms2str_ ctxt)) (get_obj g_pbl pt (fst p));

   *)

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;

"ctree.sml-------------- get_allpos' new ------------------------\"";

val (PP, pp) = split_last [1];

val ((pt', cuts), clevup) = cut_bottom (PP, pp) (get_nd pt PP);

val cuts = get_allp [] ([], ([],Frm)) pt;

val cuts2 = get_allps [] [1] (children pt);

"ctree.sml-------------- cut_tree new (from ptree above)----------";

val (pt', cuts) = cut_tree pt ([1],Frm);

"ctree.sml-------------- cappend on complete ctree from above ----";

val (pt', cuts) = cappend_form pt [1] (e_istate, e_ctxt) (str2term "Inform[1]");

"----------------------------------------------------------------/";

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

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

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

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

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

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 (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", "solve_linear"])*)

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

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

val (p,_,f,nxt,_,pt) = me nxt p [1] pt(*cappend_atomic: pos =[3,2]*);

val (p,_,f,nxt,_,pt) = me nxt p [1] pt(*.append_result: pos =[3]*);

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

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

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

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

else error "new behaviour in test: miniscript with mini-subpbl";

 show_pt pt;

"-------------- get_allpos' (from ptree above)--------------------";

"-------------- get_allpos' (from ptree above)--------------------";

"-------------- get_allpos' (from ptree above)--------------------";

if get_allpos' ([], 1) pt = 

   [([], Frm), 

    ([1], Frm), 

    ([1], Res), 

    ([2], Res), 

    ([3], Frm), 

    ([3, 1], Frm),

    ([3, 1], Res), 

    ([3, 2], Res), 

    ([3], Res), 

    ([4], Res), 

    ([], Res)]

then () else error "ctree.sml: diff:behav. in get_allpos' 1";

if get_allpos's ([], 1) (children pt) = 

   [([1], Frm), 

    ([1], Res), 

    ([2], Res), 

    ([3], Frm), 

    ([3, 1], Frm),

    ([3, 1], Res), 

    ([3, 2], Res), 

    ([3], Res), 

    ([4], Res)]

then () else error "ctree.sml: diff:behav. in get_allpos' 2";

if get_allpos's ([], 2) (takerest (1, children pt)) = 

   [([2], Res), 

    ([3], Frm), 

    ([3, 1], Frm), 

    ([3, 1], Res), 

    ([3, 2], Res),

    ([3], Res), 

    ([4], Res)]

then () else error "ctree.sml: diff:behav. in get_allpos' 3";

if get_allpos's ([], 3) (takerest (2, children pt)) = 

   [([3], Frm), 

    ([3, 1], Frm),

    ([3, 1], Res),

    ([3, 2], Res),

    ([3], Res),

    ([4], Res)]

then () else error "ctree.sml: diff:behav. in get_allpos' 4";

if get_allpos's ([3], 1) (children (nth 3 (children pt))) = 

   [([3, 1], Frm),

    ([3, 1], Res),

    ([3, 2], Res)]

then () else error "ctree.sml: diff:behav. in get_allpos' 5";

if get_allpos' ([3], 1) (nth 3 (children pt)) = 

   [([3], Frm),

    ([3, 1], Frm),

    ([3, 1], Res),

    ([3, 2], Res),

    ([3], Res)]

then () else error "ctree.sml: diff:behav. in get_allpos' 6";

"-------------- cut_level (from ptree above)----------------------";

"-------------- cut_level (from ptree above)----------------------";

"-------------- cut_level (from ptree above)----------------------";

show_pt pt;

show_pt pt';

print_depth 99; cuts; print_depth 3;

(*if cuts = [([2], Res),

	   ([3], Frm),

	   ([3, 1], Frm),

	   ([3, 1], Res),

	   ([3, 2], Res),

	   ([3], Res),

	   ([4], Res)]

then () else error "ctree.sml: diff:behav. in cut_level 1a";

val (res,asm) = get_obj g_result pt' [2];

if res = e_term andalso asm = [] then () else

error "ctree.sml: diff:behav. in cut_level 1aa" WN050219*);

if not (existpt [2] pt') then () else

error "ctree.sml: diff:behav. in cut_level 1aa2" (*WN050220*);

val (res,asm) = get_obj g_result pt' [];

(*============ inhibit exn AK110726 ==============================================

if term2str res = "[x = 1]" (*WN050219 e_term in cut_tree!!!*) then () else

error "ctree.sml: diff:behav. in cut_level 1ab";

if map fst (get_interval ([],Frm) ([],Res) 9999 pt') =

   [([], Frm), 

    ([1], Frm), 

    ([1], Res), 

    ([2], Res),(*, e_term in cut_tree!!!*)

    ([], Res)] then () else 

error "ctree.sml: diff:behav. in cut_level 1b";

============ inhibit exn AK110726 ==============================================*)

val (pt',cuts) = cut_level [] [] pt ([2],Res);

if cuts = [([3], Frm), 

	   ([3, 1], Frm), 

	   ([3, 1], Res), 

	   ([3, 2], Res), 

	   ([3], Res), 

	   ([4], Res)]

then () else error "ctree.sml: diff:behav. in cut_level 2a";

if pr_ptree pr_short pt' = ".    ----- pblobj -----\n1.   x + 1 = 2\n2.   x + 1 + -1 * 2 = 0\n"

then () else error "ctree.sml: diff:behav. in cut_level 2b";

val (pt',cuts) = cut_level [] [3] pt ([3,1],Frm);

if cuts = [([3, 1], Res), ([3, 2], Res)]

then () else error "ctree.sml: diff:behav. in cut_level 3a";

if pr_ptree pr_short pt' = ".    ----- pblobj -----\n1.   x + 1 = 2\n2.   x + 1 + -1 * 2 = 0\n3.    ----- pblobj -----\n3.1.   -1 + x = 0\n4.   [x = 1]\n"

then () else error "ctree.sml: diff:behav. in cut_level 3b";

val (pt',cuts) = cut_level [] [3] pt ([3,1],Res);

if cuts = [([3, 2], Res)]

then () else error "ctree.sml: diff:behav. in cut_level 4a";

if pr_ptree pr_short pt' = ".    ----- pblobj -----\n1.   x + 1 = 2\n2.   x + 1 + -1 * 2 = 0\n3.    ----- pblobj -----\n3.1.   -1 + x = 0\n4.   [x = 1]\n"

then () else error "ctree.sml: diff:behav. in cut_level 4b";

"-------------- cut_tree (from ptree above)-----------------------";

"-------------- cut_tree (from ptree above)-----------------------";

"-------------- cut_tree (from ptree above)-----------------------";

val (pt', cuts) = cut_tree pt ([2],Frm);(*not created by move_dn -- not on WS*)

(*============ inhibit exn AK110726 ==============================================

if cuts = [([2], Res),

	   ([3], Frm),

	   ([3, 1], Frm),

	   ([3, 1], Res),

	   ([3, 2], Res),

	   ([3], Res),

	   ([4], Res),

	   ([], Res)]

then () else error "ctree.sml: diff:behav. in cut_tree 1a";

val (res,asm) = get_obj g_result pt' [2];

============ inhibit exn AK110726 ==============================================*)

if res = e_term (*WN050219 done by cut_level*) then () else

error "ctree.sml: diff:behav. in cut_tree 1aa";

(*============ inhibit exn AK110726 ==============================================

val form = get_obj g_form pt' [2];

if term2str form = "x + 1 + -1 * 2 = 0" (*remained !!!*) then () else

error "ctree.sml: diff:behav. in cut_tree 1ab";

============ inhibit exn AK110726 ==============================================*)

val (res,asm) = get_obj g_result pt' [];

if res = e_term (*WN050219 done by cut_tree*) then () else

error "ctree.sml: diff:behav. in cut_tree 1ac";

if map fst (get_interval ([],Frm) ([],Res) 9999 pt') =

   [([], Frm), 

    ([1], Frm), 

    ([1], Res)] then () else 

error "ctree.sml: diff:behav. in cut_tree 1ad";

val (pt', cuts) = cut_tree pt ([2],Res);

(*============ inhibit exn AK110726 ==============================================

if cuts = [([3], Frm),

	   ([3, 1], Frm),

	   ([3, 1], Res),

	   ([3, 2], Res),

	   ([3], Res),

	   ([4], Res),

	   ([], Res)]

then () else error "ctree.sml: diff:behav. in cut_tree 2";

============ inhibit exn AK110726 ==============================================*)

val (pt', cuts) = cut_tree pt ([3,1],Frm);

(*============ inhibit exn AK110726 ==============================================

if cuts = [([3, 1], Res), 

	   ([3, 2], Res),

	   ([3], Res),

	   ([4], Res),

	   ([], Res)]

then () else error "ctree.sml: diff:behav. in cut_tree 3";

============ inhibit exn AK110726 ==============================================*)

val (pt', cuts) = cut_tree pt ([3,1],Res);

if cuts = [([3, 2], Res),

	   ([3], Res),

	   ([4], Res),

	   ([], Res)]

then () else error "ctree.sml: diff:behav. in cut_tree 4";

"=====new ptree 1a miniscript with mini-subpbl ===================";

"=====new ptree 1a miniscript with mini-subpbl ===================";

"=====new ptree 1a miniscript with mini-subpbl ===================";

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 (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;

show_pt pt;

"-------------- cut_level ( ,Frm) on Incomplete Nd ---------------";

"-------------- cut_level ( ,Frm) on Incomplete Nd ---------------";

"-------------- cut_level ( ,Frm) on Incomplete Nd ---------------";

val (pt',cuts) = cut_level [] [3] pt ([1],Frm);(*([1],Frm) is stored*)

if cuts = [](*([1],Res) is not yet stored (Nd.ostate=Incomplete)*)

then () else error "ctree.sml: diff:behav. in cut_tree 4a";

val (pt', cuts) = cut_tree pt ([1],Frm);

if cuts = []

then () else error "ctree.sml: diff:behav. in cut_tree 4a";

(*WN050219

val pos as ([p],_) = ([1],Frm);

val pt as Nd (b,_) = pt;

show_pt pt;

show_pt pt';

print_depth 99;cuts;print_depth 3;

print_depth 99;map fst (get_interval ([],Frm) ([],Res) 9999 pt');print_depth 3;

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

"=====new ptree 2 miniscript with mini-subpbl ====================";

"=====new ptree 2 miniscript with mini-subpbl ====================";

"=====new ptree 2 miniscript with mini-subpbl ====================";

 states:=[];

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

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

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

 Iterator 1; moveActiveRoot 1;

 autoCalculate 1 CompleteCalc; 

 interSteps 1 ([3,2],Res);

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

 show_pt pt;

if (term2str o fst) (get_obj g_result pt [3,2,1]) = "x = 0 + 1" then ()

else error "mini-subpbl interSteps broken";

"-------------- cut_tree (intermedi.ptree: 3rd level)-------------";

"-------------- cut_tree (intermedi.ptree: 3rd level)-------------";

"-------------- cut_tree (intermedi.ptree: 3rd level)-------------";

(*WN050225 intermed. outcommented

 val (pt', cuts) = cut_tree pt ([3,2,1],Frm);

 if cuts = [([3, 2, 1], Res),

	    ([3, 2, 2], Res),

	    ([3, 2], Res), 

	    ([3], Res),

	    ([4], Res)]

 then () else error "ctree.sml: diff:behav. in cut_tree 3rd level 1";

 val (pt', cuts) = cut_tree pt ([3,2,1],Res);

 if cuts = [([3, 2, 2], Res),

	    ([3, 2], Res), 

	    ([3], Res),

	    ([4], Res)]

 then () else error "ctree.sml: diff:behav. in cut_tree 3rd level 2";

"-------------- cappend (from ptree above)------------------------";

"-------------- cappend (from ptree above)------------------------";

"-------------- cappend (from ptree above)------------------------";

val (pt',cuts) = cappend_form pt [3,2,1] e_istate (str2term "newnew");

if cuts = [([3, 2, 1], Res),

	   ([3, 2, 2], Res),

	   ([3, 2], Res), 

	   ([3], Res),

	   ([4], Res),

	   ([], Res)]

then () else error "ctree.sml: diff:behav. in cappend_form";

if term2str (get_obj g_form pt' [3,2,1]) = "newnew" andalso

   get_obj g_tac pt' [3,2,1] = Empty_Tac andalso

   term2str (fst (get_obj g_result pt' [3,2,1])) = "??.empty"

 then () else error "ctree.sml: diff:behav. in cappend 1";

val (pt',cuts) = cappend_atomic pt [3,2,1] e_istate (str2term "newform")

    (Tac "test") (str2term "newresult",[]) Complete;

if cuts = [([3, 2, 1], Res), (*?????????????*)

	   ([3, 2, 2], Res),

	   ([3, 2], Res),

	   ([3], Res),

	   ([4], Res),

	   ([], Res)]

then () else error "ctree.sml: diff:behav. in cappend_atomic";

"-------------- cappend minisubpbl -------------------------------";

"-------------- cappend minisubpbl -------------------------------";

"-------------- cappend minisubpbl -------------------------------";

"=====new ptree 1 miniscript with mini-subpbl ====================";

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 (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];

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

(* nxt = Add_Given "equality (x + 1 = 2)"

   (writeln o (itms2str_ ctxt)) (get_obj g_pbl pt (fst p));

   *)

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

(* (writeln o (itms2str_ ctxt)) (get_obj g_pbl pt (fst p));

   *)

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

(* (writeln o (itms2str_ ctxt)) (get_obj g_pbl pt (fst p));

   *)

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;

(*###cappend_form: pos =[1]  ... while calculating nxt, which pt is dropped

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

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

val p = ([1], Frm);

val (pt,cuts) = cappend_form pt (fst p) e_istate (str2term "x + 1 = 2");

val form = get_obj g_form pt (fst p);

val (res,_) = get_obj g_result pt (fst p);

if term2str form = "x + 1 = 2" andalso res = e_term then () else

error "ctree.sml, diff.behav. cappend minisubpbl ([1],Frm)";

if not (existpt ((lev_on o fst) p) pt) then () else

error "ctree.sml, diff.behav. cappend minisubpbl ([1],Frm) nxt";

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

val p = ([1], Res);

val (pt,cuts) = 

    cappend_atomic pt (fst p) e_istate (str2term "x + 1 = 2")

		   Empty_Tac (str2term "x + 1 + -1 * 2 = 0",[]) Incomplete;

val form = get_obj g_form pt (fst p);

val (res,_) = get_obj g_result pt (fst p);

if term2str form = "x + 1 = 2" andalso term2str res = "x + 1 + -1 * 2 = 0" 

then () else error "ctree.sml, diff.behav. cappend minisubpbl ([1],Res)";

if not (existpt ((lev_on o fst) p) pt) then () else

error "ctree.sml, diff.behav. cappend minisubpbl ([1],Res) nxt";

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

val p = ([2], Res);

val (pt,cuts) = 

    cappend_atomic pt (fst p) e_istate (str2term "x + 1 + -1 * 2 = 0")

		   Empty_Tac (str2term "-1 + x = 0",[]) Incomplete;

val form = get_obj g_form pt (fst p);

val (res,_) = get_obj g_result pt (fst p);

if term2str form = "x + 1 + -1 * 2 = 0" andalso term2str res = "-1 + x = 0"

then () else error "ctree.sml, diff.behav. cappend minisubpbl ([2],Res)";

if not (existpt ((lev_on o fst) p) pt) then () else

error "ctree.sml, diff.behav. cappend minisubpbl ([2],Res) nxt";

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

val p = ([3], Pbl);

val (pt,cuts) = cappend_problem pt (fst p) e_istate e_fmz ([],e_spec,e_term);

if is_pblobj (get_obj I pt (fst p)) then () else 

error "ctree.sml, diff.behav. cappend minisubpbl ([3],Pbl)";

if not (existpt ((lev_on o fst) p) pt) then () else

error "ctree.sml, diff.behav. cappend minisubpbl ([3],Pbl) nxt";

(* ...complete calchead skipped...*)

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

val p = ([3, 1], Frm);

val (pt,cuts) = cappend_form pt (fst p) e_istate (str2term "-1 + x = 0");

val form = get_obj g_form pt (fst p);

val (res,_) = get_obj g_result pt (fst p);

if term2str form = "-1 + x = 0" andalso res = e_term then () else

error "ctree.sml, diff.behav. cappend minisubpbl ([3,1],Frm)";

if not (existpt ((lev_on o fst) p) pt) then () else

error "ctree.sml, diff.behav. cappend minisubpbl ([3,1],Frm) nxt";

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

val p = ([3, 1], Res);

val (pt,cuts) = 

    cappend_atomic pt (fst p) e_istate (str2term "-1 + x = 0")

		   Empty_Tac (str2term "x = 0 + -1 * -1",[]) Incomplete;

val form = get_obj g_form pt (fst p);

val (res,_) = get_obj g_result pt (fst p);

if term2str form = "-1 + x = 0" andalso term2str res = "x = 0 + -1 * -1" then()

else error "ctree.sml, diff.behav. cappend minisubpbl ([3,1],Res)";

if not (existpt ((lev_on o fst) p) pt) then () else

error "ctree.sml, diff.behav. cappend minisubpbl ([3,1],Res) nxt";

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

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

(*val (p,_,f,nxt,_,pt) = me nxt p [1] pt(**)cappend_atomic: pos =[3,2]*);

(*val (p,_,f,nxt,_,pt) = me nxt p [1] pt(**).append_result: pos =[3]*);

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

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

WN050225 intermed. outcommented---*)

"=====new ptree 3 ================================================";

"=====new ptree 3 ================================================";

"=====new ptree 3 ================================================";

states:=[];

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

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

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

 Iterator 1; moveActiveRoot 1;

 autoCalculate 1 CompleteCalc; 

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

 show_pt pt;

"-------------- move_dn ------------------------------------------";

"-------------- move_dn ------------------------------------------";

"-------------- move_dn ------------------------------------------";

 val p = move_dn [] pt ([],Pbl) (*-> ([1],Frm)*);

 val p = move_dn [] pt p        (*-> ([1],Res)*);

 val p = move_dn [] pt p        (*-> ([2],Res)*);

 val p = move_dn [] pt p        (*-> ([3],Pbl)*);

 val p = move_dn [] pt p        (*-> ([3,1],Frm)*);

 val p = move_dn [] pt p        (*-> ([3,1],Res)*);

 val p = move_dn [] pt p        (*-> ([3,2],Res)*);

 val p = move_dn [] pt p        (*-> ([3],Res)*);

(* term2str (get_obj g_res pt [3]);

   term2str (get_obj g_form pt [4]);

   *)

 val p = move_dn [] pt p        (*-> ([4],Res)*);

 val p = move_dn [] pt p        (*-> ([],Res)*);

(*

 val p = (move_dn [] pt p) handle e => print_exn_G e;

                                  Exception PTREE end of calculation*)

if p=([],Res) then () else error "ctree.sml: diff:behav. in move_dn";

"-------------- move_dn: Frm -> Res ------------------------------";

"-------------- move_dn: Frm -> Res ------------------------------";

"-------------- move_dn: Frm -> Res ------------------------------";

 states := [];

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

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

       ("Test", 

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

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

 Iterator 1; moveActiveRoot 1;

 autoCalculate 1 CompleteCalcHead;

 autoCalculate 1 (Step 1);

 refFormula 1 (get_pos 1 1);

 moveActiveRoot 1;

 moveActiveDown 1;

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

 else error "ctree.sml: diff.behav. in move_dn: Frm -> Res (1)";

 moveActiveDown 1; (*<ERROR> pos does not exist </ERROR>*)

 autoCalculate 1 (Step 1);

 refFormula 1 (get_pos 1 1);

 moveActiveDown 1; (*<ERROR> pos does not exist </ERROR>*)

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

 else error "ctree.sml: diff.behav. in move_dn: Frm -> Res (1)";

 moveActiveDown 1; (*<ERROR> pos does not exist </ERROR>*)

"-------------- move_up ------------------------------------------";

"-------------- move_up ------------------------------------------";

"-------------- move_up ------------------------------------------";

 val p = move_up [] pt ([],Res); (*-> ([4],Res)*)

 val p = move_up [] pt p;        (*-> ([3],Res)*)

 val p = move_up [] pt p;        (*-> ([3,2],Res)*)

 val p = move_up [] pt p;        (*-> ([3,1],Res)*)

 val p = move_up [] pt p;        (*-> ([3,1],Frm)*)

 val p = move_up [] pt p;        (*-> ([3],Pbl)*)

 val p = move_up [] pt p;        (*-> ([2],Res)*)

 val p = move_up [] pt p;        (*-> ([1],Res)*)

 val p = move_up [] pt p;        (*-> ([1],Frm)*)

 val p = move_up [] pt p;        (*-> ([],Pbl)*)

(*val p = (move_up [] pt p) handle e => print_exn_G e;

                                  Exception PTREE begin of calculation*)

if p=([],Pbl) then () else error "ctree.sml: diff.behav. in move_up";

"------ move into detail -----------------------------------------";

"------ move into detail -----------------------------------------";

"------ move into detail -----------------------------------------";

 states:=[];

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

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

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

 Iterator 1; moveActiveRoot 1;

 autoCalculate 1 CompleteCalc; 

 moveActiveRoot 1; 

 moveActiveDown 1;

 moveActiveDown 1;

 moveActiveDown 1; 

 refFormula 1 (get_pos 1 1) (* 2 Res, <ISA> -1 + x = 0 </ISA> *);

 interSteps 1 ([2],Res);

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

 val p = get_pos 1 1;

 val p = move_up [] pt p;     (*([2, 6], Res)*);

 val p = movelevel_up [] pt p;(*([2], Frm)*);

 val p = move_dn [] pt p;     (*([2, 1], Frm)*); 

 val p = move_dn [] pt p;     (*([2, 1], Res)*);

 val p = move_dn [] pt p;     (*([2, 2], Res)*);

 val p = move_dn [] pt p;     (*([2, 3], Res)*);

 val p = move_dn [] pt p;     (*([2, 4], Res)*);

 val p = move_dn [] pt p;     (*([2, 5], Res)*);

 val p = move_dn [] pt p;     (*([2, 6], Res)*); 

 if p = ([2, 6], Res) then() 

 else error "ctree.sml: diff.behav. in move into detail";

"=====new ptree 3a ===============================================";

"=====new ptree 3a ===============================================";

"=====new ptree 3a ===============================================";

 states:=[];

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

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

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

 Iterator 1; moveActiveRoot 1;

 autoCalculate 1 CompleteCalcHead; 

 autoCalculate 1 (Step 1); 

 autoCalculate 1 (Step 1); 

 autoCalculate 1 (Step 1);

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

 val p = move_dn [] pt ([],Pbl)       (*-> ([1], Frm)*); 

 val p = move_dn [] pt ([1], Frm)     (*-> ([1], Res)*); 

 val p = move_dn [] pt ([1], Res)     (*-> ([2], Res)*); 

 (*val p = move_dn [] pt ([2], Res)     ->Exception- PTREE "[] not complete"*);

 moveDown 1 ([],Pbl)        (*-> ([1], Frm)*);

 moveDown 1 ([1],Frm)       (*-> ([1],Res)*);

 moveDown 1 ([1],Res)       (*-> ([2],Res)*);

 moveDown 1 ([2],Res)       (*-> pos does not exist*);

(*

 get_obj g_ostate pt [1];

 show_pt pt; 

*)

"-------------- move_dn in Incomplete ctree ----------------------";

"-------------- move_dn in Incomplete ctree ----------------------";

"-------------- move_dn in Incomplete ctree ----------------------";

"=====new ptree 4: crooked by cut_level_'_ =======================";

"=====new ptree 4: crooked by cut_level_'_ =======================";

"=====new ptree 4: crooked by cut_level_'_ =======================";

states:=[];

CalcTree

[(["equality (x/(x^2 - 6*x+9) - 1/(x^2 - 3*x) =1/x)",

	   "solveFor x","solutions L"], 

  ("RatEq",["univariate","equation"],["no_met"]))];

Iterator 1; moveActiveRoot 1;

autoCalculate 1 CompleteCalc; 

getTactic 1 ([1],Res);(*Rewrite_Set RatEq_simplify*)

getTactic 1 ([2],Res);(*Rewrite_Set norm_Rational*)

getTactic 1 ([3],Res);(*Rewrite_Set RatEq_eliminate*)

getTactic 1 ([4,1],Res);(*Rewrite all_left*)

getTactic 1 ([4,2],Res);(*Rewrite_Set expand_binoms*)

getTactic 1 ([4,3],Res);(*Rewrite_Set_Inst make_ratpoly_in*)

moveActiveFormula 1 ([1],Res)(*1.1...1.4*);

moveActiveFormula 1 ([2],Res)(**ME_Isa: 'expand' not known*);

moveActiveFormula 1 ([3],Res)(*3.1.*);

moveActiveFormula 1 ([4,2],Res)(*4.2.1.*);

moveActiveFormula 1 ([4,3],Res)(**one_scr_arg: called by Script Stepwise t_=*);

moveActiveFormula 1 ([1],Res)(*1.1...1.4*);

interSteps 1 ([1],Res)(*..is activeFormula !?!*);

getTactic 1 ([1,1],Res);(*Rewrite real_diff_minus*)

getTactic 1 ([1,2],Res);(*Rewrite real_diff_minus*)

getTactic 1 ([1,3],Res);(*Rewrite real_diff_minus*)

getTactic 1 ([1,4],Res);(*Rewrite real_rat_mult_1*)

moveActiveFormula 1 ([4,2],Res)(*4.2.1.*);

interSteps 1 ([4,2],Res)(*..is activeFormula !?!*);

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

writeln(pr_ptree pr_short pt);

(*delete [4,1] in order to make pos [4],[4,4] for pblobjs differen [4],[4,3]:

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

val (pt, ppp) = cut_level_'_ [] [] pt ([4,1],Frm);

writeln(pr_ptree pr_short pt);

"-------------- get_interval from ctree: incremental development--";

"-------------- get_interval from ctree: incremental development--";

"-------------- get_interval from ctree: incremental development--";

"--- level 1: get pos from start b to end p ----------------------";

"--- level 1: get pos from start b to end p ----------------------";

"--- level 1: get pos from start b to end p ----------------------";

(******************************************************************)

(**)            val SAVE_get_trace = get_trace;                 (**)

(******************************************************************)

(*'getnds' below is structured as such:*)

fun www _ [x] = "l+r-margin"

  | www true [x1,x2] = "l-margin,  r-margin"

  | www _ [x1,x2] = "intern,  r-margin"

  | www true (x::(xs as _::_)) = "l-margin  " ^ www false xs

  | www _ (x::(xs as _::_)) = "intern  " ^ www false xs;

www true [1,2,3,4,5];

(*val it = "from  intern  intern  intern  to" : string*)

www true [1,2];

(*val it = "from  to" : string*)

www true [1];

(*val it = "from+to" : string*)

local

(*specific values of hd of pos p,q for simple handling take_fromto,

  from-pos p, to-pos q: take_fromto (hdp p) (hdq q) (children pt) ...

  ... can be used even for positions _below_ p or q*)

fun hdp [] = 1     | hdp [0] = 1     | hdp x = hd x;(*start with first*)

fun hdq	[] = 99999 | hdq [0] = 99999 | hdq x = hd x;(*take until last*)

(*analoguous for tl*)

fun tlp [] = [0]     | tlp [_] = [0]     | tlp x = tl x;

fun tlq [] = [99999] | tlq [_] = [99999] | tlq x = tl x;

(*see modspec.sml#pt_form

fun pt_form (PrfObj {form,...}) = term2str form

  | pt_form (PblObj {probl,spec,origin=(_,spec',_),...}) =

    let val (dI, pI, _) = get_somespec' spec spec'

	val {cas,...} = get_pbt pI

    in case cas of

	   NONE => term2str (pblterm dI pI)

	 | SOME t => term2str (subst_atomic (mk_env probl) t)

    end;

*)

(*.get an 'interval' from ptree down to a certain level

   by 'take_fromto children' of the nodes with specific 'from' and 'to';

   'i > 0' suppresses output during recursive descent towards 'from'

   b: the 'from' incremented to the actual pos

   p,q: specific 'from','to' for simple use of 'take_fromto'*)

fun getnd i (b,p) q (Nd (po, nds)) =

    (if  i <= 0 then [(*[(b, pt_form po)]*) (**)[b](**)] else [])

    @ (writeln("getnd  : b="^(ints2str' b)^", p="^

	       (ints2str' p)^", q="^(ints2str' q));

       getnds (i-1) true (b@[hdp p], tlp p) (tlq q)

	       (take_fromto (hdp p) (hdq q) nds))

and getnds _ _ _ _ [] = []                         (*no children*)

  | getnds i _ (b,p) q [nd] = (getnd i (b,p) q nd) (*l+r-margin*)

  | getnds i true (b,p) q [n1, n2] =               (*l-margin,  r-margin*)

    (writeln("getnds3: b="^ ints2str' b ^", p="^ ints2str' p ^

	     ", q="^ ints2str' q);

    (getnd i      (       b, p ) [99999] n1) @

    (getnd ~99999 (lev_on b,[0]) q       n2))

  | getnds i _    (b,p) q [n1, n2] =               (*intern,  r-margin*)

    (writeln("getnds4: b="^ ints2str' b ^", p="^ ints2str' p ^

	     ", q="^ ints2str' q);

    (getnd i      (       b,[0]) [99999] n1) @

    (getnd ~99999 (lev_on b,[0]) q       n2))

  | getnds i true (b,p) q (nd::(nds as _::_)) =    (*l-margin, intern*)

    (writeln("getnds5: b="^ ints2str' b ^", p="^ ints2str' p ^

	     ", q="^ ints2str' q);

    (getnd i             (       b, p ) [99999] nd) @

    (getnds ~99999 false (lev_on b,[0]) q nds)) 

  | getnds i _ (b,p) q (nd::(nds as _::_)) =       (*intern, ...*)

    (getnd i             (       b,[0]) [99999] nd) @

    (getnds ~99999 false (lev_on b,[0]) q nds); 

in

(*get an 'interval from to' from a ptree as 'intervals f t' of respective nodes

  where 'from' are pos, i.e. a key as int list, 'f' an int (to,t analoguous)

(1) the 'f' are given 

(1a) by 'from' if 'f' = the respective element of 'from' (left margin)

(1b) -inifinity, if 'f' > the respective element of 'from' (internal node)

(2) the 't' ar given

(2a) by 'to' if 't' = the respective element of 'to' (right margin)

(2b) inifinity, if 't' < the respective element of 'to (internal node)'

the 'f' and 't' are set by hdp,... *)

fun get_trace pt p q =

    (flat o (getnds ((length p) -1) true ([hdp p], tlp p) (tlq q))) 

	(take_fromto (hdp p) (hdq q) (children pt));

end;

writeln(pr_ptree pr_short pt);

case get_trace pt [1,3] [4,1,1] of

    [[1,3],[1,4],[2],[3],[4],[4,1],[4,1,1]] => () 

  | _ => error "diff.behav.in ctree.sml: get_interval lev 1a";

case get_trace pt [2] [4,3,2] of

    [[2],[3],[4],[4,1],[4,1,1],[4,2],[4,3],[4,3,1],[4,3,2]] => ()

  | _ => error "diff.behav.in ctree.sml: get_interval lev 1b";

case get_trace pt [1,4] [4,3,1] of

    [[1,4],[2],[3],[4],[4,1],[4,1,1],[4,2],[4,3],[4,3,1]] => () 

  | _ => error "diff.behav.in ctree.sml: get_interval lev 1c";

(*========== inhibit exn AK110719 ==============================================

case get_trace pt [4,2] [5] of

   (*[([4,2],_),([4,3],_),([4,4],_),([4,4,1],_),([4,4,2],_),([4,4,3],_),

    ([4,4,4],_),([4,4,5],_),([5],_)] => () ..with pt_form*)

    [[4,2],[4,3],[4,3,1],[4,3,2],[4,3,3],[4,3,4],[4,3,5],[5]]=>()

  | _ => error "diff.behav.in ctree.sml: get_interval lev 1d";

========== inhibit exn AK110719 ==============================================*)

case get_trace pt [] [4,4,2] of

    [[1],[1,1],[1,2],[1,3],[1,4],[2],[3],[4],[4,1],[4,1,1],[4,2],

     [4,3],[4,3,1],[4,3,2]] => () 

  | _ => error "diff.behav.in ctree.sml: get_interval lev 1e";

(*========== inhibit exn AK110719 ==============================================

case get_trace pt [] [] of

    [[1],[1,1],[1,2],[1,3],[1,4],[2],[3],[4],[4,1],[4,1,1],[4,2],

     [4,3],[4,3,1],[4,3,2],[4,3,3],[4,3,4],[4,3,5],[5]] => () 

  | _ => error "diff.behav.in ctree.sml: get_interval lev 1f";

case get_trace pt [4,3] [4,3] of

    [[4,3],[4,3,1],[4,3,2],[4,3,3],[4,3,4],[4,3,5]] => () 

  | _ => error "diff.behav.in ctree.sml: get_interval lev 1g";

========== inhibit exn AK110719 ==============================================*)

"--- level 2: get pos' from start b to end p ---------------------";

"--- level 2: get pos' from start b to end p ---------------------";

"--- level 2: get pos' from start b to end p ---------------------";

(*idea: pos_ is _ONLY_ relevant exactly at (endpoint of) from, to

  development stopped in favour of move_dn, see get_interval

  actually used (inefficient) version with move_dn: see modspec.sml

*)

(*

case get_trace pt ([1,4],Res) ([4,4,1],Frm) of

    [[2],[3],[4],[4,1],[4,2],[4,2,1],[4,3],[4,4],[4,4,1]] => () 

  | _ => error "diff.behav.in ctree.sml: get_interval lev 1b";

case get_trace pt ([],Pbl) ([],Res) of

    [[1],[1,1],[1,2],[1,3],[1,4],[2],[3],[4],[4,1],[4,2],[4,2,1],[4,3],

     [4,4],[4,4,1],[4,4,2],[4,4,3],[4,4,4],[4,4,5],[5]] => () 

  | _ => error "diff.behav.in ctree.sml: get_interval lev 1e";

*)

(******************************************************************)

(**)            val get_trace = SAVE_get_trace;                 (**)

(******************************************************************)

"=====new ptree 4 ratequation ====================================";

"=====new ptree 4 ratequation ====================================";

"=====new ptree 4 ratequation ====================================";

states:=[];

CalcTree

[(["equality (x/(x^2 - 6*x+9) - 1/(x^2 - 3*x) =1/x)",

	   "solveFor x","solutions L"], 

  ("RatEq",["univariate","equation"],["no_met"]))];

Iterator 1; moveActiveRoot 1;

autoCalculate 1 CompleteCalc; 

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

show_pt pt;

"-------------- pt_extract form, tac, asm<>[] --------------------";

"-------------- pt_extract form, tac, asm<>[] --------------------";

"-------------- pt_extract form, tac, asm<>[] --------------------";

val (Form form, SOME tac, asm) = pt_extract (pt, ([3], Res));

case (term2str form, tac, terms2strs asm) of

    ("(3 + -1 * x + x ^^^ 2) * x = 1 * (9 * x + -6 * x ^^^ 2 + x ^^^ 3)",

     Subproblem

         ("PolyEq",

          ["normalize", "polynomial", "univariate", "equation"]),

	 ["9 * x + -6 * x ^^^ 2 + x ^^^ 3 ~= 0"]) => ()

  | _ => error "diff.behav.in ctree.sml: pt_extract asm<>[]";

(*WN060717 unintentionally changed some rls/ord while 

     completing knowl. for thes2file...

  case (term2str form, tac, terms2strs asm) of

    ((*"(3 + (-1 * x + x ^^^ 2)) * x = 1 * (9 * x + (x ^^^ 3 + -6 * x ^^^ 2))",

     *)Subproblem

         ("PolyEq",

          ["normalize", "polynomial", "univariate", "equation"]),

	 ["9 * x + (x ^^^ 3 + -6 * x ^^^ 2) ~= 0"]) => ()

  | _ => error "diff.behav.in ctree.sml: pt_extract asm<>[]";

.... but it became even better*)

"=====new ptree 5 minisubpbl =====================================";

"=====new ptree 5 minisubpbl =====================================";

"=====new ptree 5 minisubpbl =====================================";

states:=[];

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

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

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

Iterator 1; moveActiveRoot 1;

autoCalculate 1 CompleteCalc; 

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

show_pt pt;

"-------------- pt_extract form, tac, asm ------------------------";

"-------------- pt_extract form, tac, asm ------------------------";

"-------------- pt_extract form, tac, asm ------------------------";

val (ModSpec (_,_,form,_,_,_), SOME tac, asm) = pt_extract (pt, ([], Frm));

case (term2str form, tac, terms2strs asm) of

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

    Apply_Method ["Test", "squ-equ-test-subpbl1"],

     []) => ()

  | _ => error "diff.behav.in ctree.sml: pt_extract ([], Pbl)";

val (Form form, SOME tac, asm) = pt_extract (pt, ([1], Frm));

case (term2str form, tac, terms2strs asm) of

    ("x + 1 = 2", Rewrite_Set "norm_equation", []) => ()

  | _ => error "diff.behav.in ctree.sml: pt_extract ([1], Frm)";

val (Form form, SOME tac, asm) = pt_extract (pt, ([1], Res));

case (term2str form, tac, terms2strs asm) of

    ("x + 1 + -1 * 2 = 0", Rewrite_Set "Test_simplify", []) => ()

  | _ => error "diff.behav.in ctree.sml: pt_extract ([1], Res)";

val (Form form, SOME tac, asm) = pt_extract (pt, ([2], Res));

case (term2str form, tac, terms2strs asm) of

    ("-1 + x = 0",

     Subproblem ("Test", ["linear", "univariate", "equation", "test"]),

     []) => ()

  | _ => error "diff.behav.in ctree.sml: pt_extract ([2], Res)";

val (ModSpec (_,_,form,_,_,_), SOME tac, asm) = pt_extract (pt, ([3], Pbl));

case (term2str form, tac, terms2strs asm) of

    ("solve (-1 + x = 0, x)", Apply_Method ["Test", "solve_linear"], []) => ()

  | _ => error "diff.behav.in ctree.sml: pt_extract ([3], Pbl)";

val (Form form, SOME tac, asm) = pt_extract (pt, ([3,1], Frm));

case (term2str form, tac, terms2strs asm) of

    ("-1 + x = 0", Rewrite_Set_Inst (["(bdv, x)"], "isolate_bdv"), []) => ()

  | _ => error "diff.behav.in ctree.sml: pt_extract ([3,1], Frm)";

val (Form form, SOME tac, asm) = pt_extract (pt, ([3,1], Res));

case (term2str form, tac, terms2strs asm) of

    ("x = 0 + -1 * -1", Rewrite_Set "Test_simplify", []) => ()

  | _ => error "diff.behav.in ctree.sml: pt_extract ([3,1], Res)";

val (Form form, SOME tac, asm) = pt_extract (pt, ([3,2], Res));

case (term2str form, tac, terms2strs asm) of

    ("x = 1", Check_Postcond ["linear", "univariate", "equation", "test"], 

     []) => ()

  | _ => error "diff.behav.in ctree.sml: pt_extract ([3,2], Res)";

(*========== inhibit exn AK110719 ==============================================

val (Form form, SOME tac, asm) = pt_extract (pt, ([3], Res));

case (term2str form, tac, terms2strs asm) of

    ("[x = 1]", Check_elementwise "Assumptions", []) => ()

  | _ => error "diff.behav.in ctree.sml: pt_extract ([3], Res)";