# HG changeset patch
# User wneuper
# Date 1156517180 -7200
# Node ID 1d03ac072f846182845f413776675ad586de6d36
# Parent  87c4ce2d4bac4de4d25ed63fd4b2eb429d056ff5
repair reverse rewrite; has been broken by extending 'type rule' with 'Rls_'

diff -r 87c4ce2d4bac -r 1d03ac072f84 src/sml/FE-interface/interface.sml
--- a/src/sml/FE-interface/interface.sml	Thu Aug 24 12:51:16 2006 +0200
+++ b/src/sml/FE-interface/interface.sml	Fri Aug 25 16:46:20 2006 +0200
@@ -314,7 +314,6 @@
    *)
 fun interSteps cI ip =
     (let val ((pt,p), tacis) = get_calc cI
-	(*val ip = get_pos cI iI*)(*WN050215 quick and dirty*)
      in if (not o is_interpos) ip
 	then interStepsERROR cI "only formulae with position (_,Res) \
 				\may have intermediate steps above them"
diff -r 87c4ce2d4bac -r 1d03ac072f84 src/sml/IsacKnowledge/Rational.ML
--- a/src/sml/IsacKnowledge/Rational.ML	Thu Aug 24 12:51:16 2006 +0200
+++ b/src/sml/IsacKnowledge/Rational.ML	Fri Aug 25 16:46:20 2006 +0200
@@ -2783,7 +2783,7 @@
 Remark: the reverse ruleset does _NOT_ work properly with other input !.*)
 (*WN020824 wir werden "uberlegen, wie wir ungeeignete inputs zur"uckweisen*)
 
-val {rules=rules,rew_ord=(_,ro),...} =
+val {rules, rew_ord=(_,ro),...} =
     rep_rls (assoc_rls "make_polynomial");
 val thy = Rational.thy;
 
@@ -2801,18 +2801,23 @@
 	  list);      (*derivation from given term to normalform
 		       in reverse order with sym_thm;
                        (#) could be extracted from here by (map #1)*).*)
+(* val {rules=rules,rew_ord=(_,ro),...} =
+    rep_rls (assoc_rls "make_polynomial")     (*USE ALWAYS, SEE val cancel_p*);
+   val (thy, eval_rls, ro) =(Rational.thy, Atools_erls, ro) (*..val cancel_p*);
+   val t = t;
+   *)
 fun init_state thy eval_rls ro t =
-    let val Some (t',_) = factout_p_ thy t;
-        val Some (t'',asm) = cancel_p_ thy t;
-        val der = reverse_deriv thy eval_rls rules ro None t';
+    let val Some (t',_) = factout_p_ thy t
+        val Some (t'',asm) = cancel_p_ thy t
+        val der = reverse_deriv thy eval_rls rules ro None t'
         val der = der @ [(Thm ("real_mult_div_cancel2",
 			       num_str real_mult_div_cancel2),
 			  (t'',asm))]
-        val rs = (distinct_Thm o (map #1)) der;
+        val rs = (distinct_Thm o (map #1)) der
 	val rs = filter_out (eq_Thms ["sym_real_add_zero_left",
 				      "sym_real_mult_0",
-				      "sym_real_mult_1"]) rs;
-    in (t,t'',[rs(*here only _ONE_*)],der) end;
+				      "sym_real_mult_1"]) rs
+    in (t,t'',[rs(*here only _ONE_ WN060925 why?*)],der) end;
 
 (*.locate_rule = fn : rule list -> term -> rule
 		      -> (rule * (term * term list) option) list.
diff -r 87c4ce2d4bac -r 1d03ac072f84 src/sml/ME/rewtools.sml
--- a/src/sml/ME/rewtools.sml	Thu Aug 24 12:51:16 2006 +0200
+++ b/src/sml/ME/rewtools.sml	Fri Aug 25 16:46:20 2006 +0200
@@ -77,7 +77,11 @@
          term list)) : ... under these assumptions.
        list          :
 returns empty list for a normal form
-040214: FIXME treats rules as in Rls, _not_ as in Seq*)
+FIXME.WN040214: treats rules as in Rls, _not_ as in Seq
+
+WN060825 too complicated for the intended use by cancel_, common_nominator_
+and unreflectedly adapted to extion of rules by Rls_: returns Rls_("sym_simpl..
+ -- replaced below*)
 fun make_deriv thy erls (rs:rule list) ro(*rew_ord*) goal tt = 
     let
 	datatype switch = Appl | Noap;
@@ -127,11 +131,6 @@
 		     rew_once (rts @ [(t,r,(t',a'))]) t' Appl rrs');
 
     in rew_once [] tt Noap rs end;
-(*
-  val t9 = (term_of o the o (parse thy)) "(8*(-1 + x))/(9*(-1 + x))";
-  val rst = make_deriv thy eval_rls make_polynomial None t9;
-  writeln(trtas2str rst);
-*)
 
 (*.toggles the marker for 'fun sym_thm'.*)
 fun sym_thmID (thmID : thmID) =
@@ -169,7 +168,7 @@
 	  rew_ord=rew_ord};
 
 fun sym_Thm (Thm (thmID, thm)) = Thm (sym_thmID thmID, sym_thm thm)
-  | sym_Thm (Rls_ rls) = Rls_ (sym_rls rls)
+  | sym_Thm (Rls_ rls) = Rls_ (*WN060825?!?*) (sym_rls rls)
   | sym_Thm r = raise error ("sym_Thm: not for "^(rule2str r));
 (*
   val th =  Thm ("real_one_collect",num_str real_one_collect);
@@ -180,6 +179,7 @@
 ML> val it =
   Thm ("sym_real_one_collect","?m is_const ==> (1 + ?m) * ?n = ?n + ?m * ?n")*)
 
+
 (*version for reverse rewrite used before 040214*)
 fun rev_deriv (t, r, (t', a)) = (sym_Thm r, (t, a));
 fun reverse_deriv thy erls (rs:rule list) ro(*rew_ord*) goal t =
diff -r 87c4ce2d4bac -r 1d03ac072f84 src/smltest/IsacKnowledge/rational.sml
--- a/src/smltest/IsacKnowledge/rational.sml	Thu Aug 24 12:51:16 2006 +0200
+++ b/src/smltest/IsacKnowledge/rational.sml	Fri Aug 25 16:46:20 2006 +0200
@@ -33,6 +33,7 @@
 "-------- me Schalk I No.186 -------------------------------------";
 "-------- interSteps ..Simp_Rat_Double_No-1.xml ------------------";
 "-------- interSteps ..Simp_Rat_Cancel_No-1.xml ------------------";
+"-------- investigate format of factout_ and factout_p_ ----------";
 "-----------------------------------------------------------------";
 "-----------------------------------------------------------------";
 "-----------------------------------------------------------------";
@@ -2023,7 +2024,7 @@
 "-------- interSteps ..Simp_Rat_Cancel_No-1.xml ------------------";
 states:=[];
 CalcTree
-[(["term ((14 * x * y) / ( x * y ))", "normalform N"], 
+[(["term ((a^2 + -1*b^2) / (a^2 + -2*a*b + b^2))", "normalform N"], 
   ("Rational.thy",["rational","simplification"],
   ["simplification","of_rationals"]))];
 Iterator 1;
@@ -2040,4 +2041,30 @@
 (*WN060823 cancel_p_ init_state does not terminate, see Rational.ML
 interSteps 1 ([1,2,1],Res);
 val ((pt,p),_) = get_calc 1; show_pt pt;
-*)
\ No newline at end of file
+*)
+
+"-------- investigate format of factout_ and factout_p_ ----------";
+"-------- investigate format of factout_ and factout_p_ ----------";
+"-------- investigate format of factout_ and factout_p_ ----------";
+val {rules, rew_ord = (_,ro),...} = rep_rls (assoc_rls "make_polynomial");
+val (thy, eval_rls) = (Rational.thy, Atools_erls)(*see 'fun init_state'*);
+val Rrls {scr = Rfuns {init_state,...},...} = assoc_rls "cancel_p";
+
+"----- see  Rational.ML, local cancel_p, fun init_state";
+val t = str2term "(a^^^2 + (-1)*b^^^2) / (a^^^2 + (-2)*a*b + b^^^2)";
+val Some (t',_) = factout_p_ thy t; term2str t';
+(*
+val rtas = reverse_deriv thy eval_rls rules ro None t';
+writeln(trtas2str rst);
+*)
+
+
+"----- see  Rational.ML, local cancel_p, fun init_state";
+val t = str2term "a^^^2 / a";
+val Some (t',_) = factout_p_ thy t; term2str t';
+(*val it = "1 * a * (1 * a) / (1 * (1 * a))" ... can be canceled with
+           real_mult_div_cancel2 ?k ~= 0 ==> ?m * ?k / (?n * ?k) = ?m / ?n"*)
+(*
+val rtas = reverse_deriv thy eval_rls rules ro None t';
+writeln(rtas2str rtas);
+*)
diff -r 87c4ce2d4bac -r 1d03ac072f84 src/smltest/IsacKnowledge/root.sml
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/smltest/IsacKnowledge/root.sml	Fri Aug 25 16:46:20 2006 +0200
@@ -0,0 +1,15 @@
+(* testexamples for Root, radicals
+   *)
+
+val thy = Root.thy;
+
+val t = str2term "sqrt 1";
+val Some (t',_) = rewrite_set_ thy false Root_erls t;
+if term2str t' = "1" then () else raise error "root.sml: diff.behav. sqrt 1";
+val t = str2term "sqrt -1";
+val None = rewrite_set_ thy false Root_erls t;
+
+val t = str2term "sqrt 0";
+val Some (t',_) = rewrite_set_ thy false Root_erls t;
+term2str t';
+if term2str t' = "0" then () else raise error "root.sml: diff.behav. sqrt 1";
diff -r 87c4ce2d4bac -r 1d03ac072f84 src/smltest/IsacKnowledge/rootrateq.sml
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/smltest/IsacKnowledge/rootrateq.sml	Fri Aug 25 16:46:20 2006 +0200
@@ -0,0 +1,229 @@
+(* testexamples for RootratEq, equations mixing fractions and roots
+   use"rootrateq.sml";
+   *)
+
+val thy = Isac.thy;
+
+"--------------------- tests on predicates  -------------------------------";
+"--------------------- tests on predicates  -------------------------------";
+"--------------------- tests on predicates  -------------------------------";
+(* 
+ Compiler.Control.Print.printDepth:=5; (*4 default*)
+ trace_rewrite:=true;
+ trace_rewrite:=false;
+*)
+val t1 = (term_of o the o (parse thy)) "(-8 - sqrt(x) + x^^^2) is_rootRatAddTerm_in x";
+val Some (t,_) = rewrite_set_ RootRatEq.thy false RootRatEq_prls t1;
+if (term2str t) = "False" then ()
+ else  raise error "rootrateq.sml: diff.behav. 1 in is_rootRatAddTerm_in";
+
+val t1 = (term_of o the o (parse thy)) "(1/x) is_rootRatAddTerm_in x";
+val Some (t,_) = rewrite_set_ RootRatEq.thy false RootRatEq_prls t1;
+if (term2str t) = "False" then ()
+ else  raise error "rootrateq.sml: diff.behav. 2 in is_rootRatAddTerm_in";
+
+val t1 = (term_of o the o (parse thy)) "(1/sqrt(x)) is_rootRatAddTerm_in x";
+val Some (t,_) = rewrite_set_ RootRatEq.thy false RootRatEq_prls t1;
+if (term2str t) = "False" then ()
+ else  raise error "rootrateq.sml: diff.behav. 3 in is_rootRatAddTerm_in";
+
+val t1 = (term_of o the o (parse thy)) "(1/(sqrt(x)+1)) is_rootRatAddTerm_in x";
+val Some (t,_) = rewrite_set_ RootRatEq.thy false RootRatEq_prls t1;
+if (term2str t) = "True" then ()
+ else  raise error "rootrateq.sml: diff.behav. 4 in is_rootRatAddTerm_in";
+
+val t1 = (term_of o the o (parse thy)) "(3 + 1/(1+sqrt(x))) is_rootRatAddTerm_in x";
+val Some (t,_) = rewrite_set_ RootRatEq.thy false RootRatEq_prls t1;
+if (term2str t) = "True" then ()
+ else  raise error "rootrateq.sml: diff.behav. 5 in is_rootRatAddTerm_in";
+
+val t1 = (term_of o the o (parse thy)) "(1/(1+sqrt(y)) + 3 + 1/(1+sqrt(x))) is_rootRatAddTerm_in x";
+val Some (t,_) = rewrite_set_ RootRatEq.thy false RootRatEq_prls t1;
+if (term2str t) = "True" then ()
+ else  raise error "rootrateq.sml: diff.behav. 6 in is_rootRatAddTerm_in";
+
+val t1 = (term_of o the o (parse thy)) "(1/(1+sqrt(x)) + 3 + 1/(1+sqrt(y))) is_rootRatAddTerm_in x";
+val Some (t,_) = rewrite_set_ RootRatEq.thy false RootRatEq_prls t1;
+if (term2str t) = "True" then ()
+ else  raise error "rootrateq.sml: diff.behav. 7 in is_rootRatAddTerm_in";
+
+
+"--------------------- test thm rootrat_equation_left_1 ---------------------";
+val fmz = ["equality ( -2 + 1/(1 - sqrt(x))= 0)", "solveFor x","solutions L"];
+val (dI',pI',mI') = ("RootRatEq.thy",["univariate","equation"],["no_met"]);
+
+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 (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; 
+(*-> Subproblem ("RootEq.thy", ["univariate", ...])*)
+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 (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; 
+(*-> Subproblem ("RootEq.thy", ["univariate", ...])*)
+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 (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; 
+(*-> Subproblem ("RootEq.thy", ["univariate", ...])*)
+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 (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; 
+if f =  Form' (FormKF (~1, EdUndef, 0, Nundef, "1 + -4 * x = 0")) then ()
+else raise error "rootrateq.sml: diff.behav. in rootrat_equation_left_1";
+(*-> Subproblem ("RootEq.thy", ["polynomial", ...])*)
+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 (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 (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;
+case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 1 / 4]")) => ()
+	 | _ => raise error "rootrateq.sml: diff.behav. in  -2 + 1/(1 - sqrt(x))= 0 -> [x = 1/4]";
+
+"--------------------- test thm rootrat_equation_left_2 ---------------------";
+val fmz = ["equality (3/(1+sqrt(x))= 1)", "solveFor x","solutions L"];
+val (dI',pI',mI') = ("RootRatEq.thy",["univariate","equation"],["no_met"]);
+
+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 (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;
+(*-> Subproblem ("RootEq.thy", ["univariate", ...])*)
+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 (p,_,f,nxt,_,pt) = me nxt p c pt;
+val (p,_,f,nxt,_,pt) = me nxt p c pt; 
+(*-> Subproblem ("RootEq.thy", ["univariate", ...])*)
+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 (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; 
+(*-> Subproblem ("RootEq.thy", ["univariate", ...])*)
+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 (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; 
+if f = Form' (FormKF (~1, EdUndef, 0, Nundef, "4 + -1 * x = 0")) then ()
+else raise error "rootrateq.sml: diff.behav. in rootrat_equation_left_2";
+(*-> Subproblem ("PolyEq.thy", ["polynomial", ...])*)
+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 (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 (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;
+case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 4]")) => ()
+	 | _ => raise error "rootrateq.sml: diff.behav. in  3/(1+sqrt(x))= 1 -> [x = 4]";
+
+"--------------------- test thm rootrat_equation_right_1 ---------------";
+val fmz = ["equality ( 0= -2 + 1/(1 - sqrt(x)))", "solveFor x","solutions L"];
+val (dI',pI',mI') = ("RootRatEq.thy",["univariate","equation"],["no_met"]);
+
+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 (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 (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 (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 (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 (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; 
+if f = Form' (FormKF (~1, EdUndef, 0, Nundef, "-1 + 4 * x = 0")) then ()
+else raise error "rootrateq.sml: diff.behav.ppoly in rootrat_equation_right_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 (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 (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 (p,_,f,nxt,_,pt) = me nxt p c pt;
+case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 1 / 4]")) => ()
+	 | _ => raise error "rootrateq.sml: diff.behav. in  -2 + 1/(1 - sqrt(x))= 0 -> [x = 1/4]";
+
+"--------------------- test thm rootrat_equation_right_2 --------------------";
+val fmz = ["equality (1 = 3/(1+sqrt(x)))", "solveFor x","solutions L"];
+val (dI',pI',mI') = ("RootRatEq.thy",["univariate","equation"],["no_met"]);
+
+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 (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 (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 (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 (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 (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; 
+if f = Form' (FormKF (~1, EdUndef, 0, Nundef, "-4 + x = 0")) then ()
+else raise error "rootrateq.sml: diff.behav. in rootrat_equation_right_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 (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 (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;
+case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 4]")) => ()
+	 | _ => raise error "rootrateq.sml: diff.behav. in  3/(1+sqrt(x))= 1 -> [x = 4]";