neuper@37906: (* testexamples for RootratEq, equations mixing fractions and roots
neuper@42393:    WN120314 some complicated equations still are outcommented.
neuper@37906:    *)
neuper@37906: 
neuper@42393: "-----------------------------------------------------------------";
neuper@42393: "table of contents -----------------------------------------------";
neuper@42393: "-----------------------------------------------------------------";
neuper@42393: "------------ tests on predicates  -------------------------------";
neuper@42393: "------------ test thm rootrat_equation_left_1 -------------------";
neuper@42393: "------------ test thm rootrat_equation_left_2 -------------------";
neuper@42393: "------------ test thm rootrat_equation_right_1 ------------------";
neuper@42393: "------------ test thm rootrat_equation_right_2 ------------------";
neuper@42393: "-----------------------------------------------------------------";
neuper@42393: "-----------------------------------------------------------------";
neuper@41943: 
neuper@42393: val thy = @{theory "RootRatEq"};
neuper@41943: 
neuper@42393: "------------ tests on predicates  -------------------------------";
neuper@42393: "------------ tests on predicates  -------------------------------";
neuper@42393: "------------ tests on predicates  -------------------------------";
wneuper@59188: val t1 = (Thm.term_of o the o (parse thy)) "(-8 - sqrt(x) + x^^^2) is_rootRatAddTerm_in x";
neuper@42393: val SOME (t,_) = rewrite_set_ @{theory "RootRatEq"} false RootRatEq_prls t1;
neuper@42393: if (term2str t) = "False" then ()
neuper@38031:  else  error "rootrateq.sml: diff.behav. 1 in is_rootRatAddTerm_in";
neuper@37906: 
wneuper@59188: val t1 = (Thm.term_of o the o (parse thy)) "(1/x) is_rootRatAddTerm_in x";
neuper@42393: val SOME (t,_) = rewrite_set_ @{theory "RootRatEq"} false RootRatEq_prls t1;
neuper@42393: if (term2str t) = "False" then ()
neuper@38031:  else  error "rootrateq.sml: diff.behav. 2 in is_rootRatAddTerm_in";
neuper@37906: 
wneuper@59188: val t1 = (Thm.term_of o the o (parse thy)) "(1/sqrt(x)) is_rootRatAddTerm_in x";
neuper@42393: val SOME (t,_) = rewrite_set_ @{theory "RootRatEq"} false RootRatEq_prls t1;
neuper@42393: if (term2str t) = "False" then ()
neuper@38031:  else  error "rootrateq.sml: diff.behav. 3 in is_rootRatAddTerm_in";
neuper@37906: 
wneuper@59188: val t1 = (Thm.term_of o the o (parse thy)) "(1/(sqrt(x)+1)) is_rootRatAddTerm_in x";
neuper@42393: val SOME (t,_) = rewrite_set_ @{theory "RootRatEq"} false RootRatEq_prls t1;
neuper@42393: if (term2str t) = "True" then ()
neuper@38031:  else  error "rootrateq.sml: diff.behav. 4 in is_rootRatAddTerm_in";
neuper@37906: 
wneuper@59188: val t1 = (Thm.term_of o the o (parse thy)) "(3 + 1/(1+sqrt(x))) is_rootRatAddTerm_in x";
neuper@42393: val SOME (t,_) = rewrite_set_ @{theory "RootRatEq"} false RootRatEq_prls t1;
neuper@42393: if (term2str t) = "True" then ()
neuper@38031:  else  error "rootrateq.sml: diff.behav. 5 in is_rootRatAddTerm_in";
neuper@37906: 
wneuper@59188: val t1 = (Thm.term_of o the o (parse thy)) "(1/(1+sqrt(y)) + 3 + 1/(1+sqrt(x))) is_rootRatAddTerm_in x";
neuper@42393: val SOME (t,_) = rewrite_set_ @{theory "RootRatEq"} false RootRatEq_prls t1;
neuper@42393: if (term2str t) = "True" then ()
neuper@38031:  else  error "rootrateq.sml: diff.behav. 6 in is_rootRatAddTerm_in";
neuper@37906: 
wneuper@59188: val t1 = (Thm.term_of o the o (parse thy)) "(1/(1+sqrt(x)) + 3 + 1/(1+sqrt(y))) is_rootRatAddTerm_in x";
neuper@42393: val SOME (t,_) = rewrite_set_ @{theory "RootRatEq"} false RootRatEq_prls t1;
neuper@42393: if (term2str t) = "True" then ()
neuper@38031:  else  error "rootrateq.sml: diff.behav. 7 in is_rootRatAddTerm_in";
neuper@37906: 
neuper@42393: "------------ test thm rootrat_equation_left_1 -------------------";
neuper@42393: "------------ test thm rootrat_equation_left_1 -------------------";
neuper@42393: "------------ test thm rootrat_equation_left_1 -------------------";
neuper@42393: val c = [];
neuper@42393: val fmz = ["equality ( -2 + 1/(1 - sqrt(x))= (0::real))", "solveFor x","solutions L"];
neuper@37991: val (dI',pI',mI') = ("RootRatEq",["univariate","equation"],["no_met"]);
neuper@37906: val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p c pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
neuper@42398: val (p,_,f,nxt,_,pt) = me nxt p c pt;
neuper@42398: (*============ inhibit exn WN120319 ==============================================
neuper@42398: (*From final Test_Isac.thy we suddenly have
neuper@42398: 
neuper@42398:           nxt = ("Model_Problem", Model_Problem)
neuper@42398: 
neuper@42398: which we did not investigate further due to the decision to drop the whole type of equation.
neuper@42398: *)
neuper@42393: if f2str f = "1 = (0 - -2) * (1 + -1 * sqrt x)" then ()
neuper@42393: else error "rootrateq.sml: diff.behav. in rootrat_equation_left_1 a";
neuper@42393: (*-> Subproblem ("RootRatEq", ["sq", "root'", "univariate", "equation"])*)
neuper@42393: val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
neuper@42393: val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
neuper@42393: val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
neuper@42393: val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
neuper@42393: val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p''',_,f,nxt,_,pt''') = me nxt p c pt;
neuper@42393: 
neuper@42393: (*we investigate, why the next step results in Empty_Tac*)
neuper@42393: f2str f = "1 = 2 * (1 + -1 * sqrt x)";
neuper@42393: nxt = ("Rewrite_Set", Rewrite_Set "make_rooteq");
neuper@42393: (*... these ar the step's arguments; from these we do directly ...*)
neuper@42393: val SOME t = parseNEW ctxt "1 = 2 * (1 + -1 * sqrt x)"
neuper@42393: val SOME (t, _) = rewrite_set_ thy true make_rooteq t;
neuper@42393: term2str t = "1 = 2 + -2 * sqrt x";
neuper@42393: (*... which works; thus error must be in script interpretation*)
neuper@42393: 
wneuper@59279: "~~~~~ fun me, args:"; val (((_,tac):tac'_), (p:pos'), _, (pt:ctree)) = (nxt, p, c, pt);
neuper@42393: val (pt, p) = case locatetac tac (pt,p) of
neuper@42393: 	("ok", (_, _, ptp))  => ptp;
neuper@42393: "~~~~~ fun step, args:"; val (ip as (_,p_), (ptp as (pt,p), tacis)) = (p, ((pt, e_pos'), []))
neuper@42393: val pIopt = get_pblID (pt,ip);
neuper@42393: ip;    (*= ([3, 2], Res)*)
neuper@42393: tacis; (*= []*)
neuper@42393: pIopt; (*= SOME ["sq", "root'", "univariate", "equation"]*)
neuper@42393: member op = [Pbl,Met] p_ andalso is_none (get_obj g_env pt (fst p)); (*= false*)
neuper@42393: "~~~~~ fun nxt_solve_, args:"; (*stopped due to strange exn
neuper@42393:   "check_elementwise: no set 1 = 2 + -2 * sqrt x"*)
neuper@42393: 
neuper@42393: (*---- 2nd try: we investigate the script ["RootEq","solve_sq_root_equation"] found via pbl*)
neuper@42393: val t = str2term "((lhs e_e) is_sqrtTerm_in v_v) | ((rhs e_e) is_sqrtTerm_in v_v)";
neuper@42393: val t = str2term ("((lhs (1 = 2 * (1 + -1 * sqrt x))) is_sqrtTerm_in x) |" ^
neuper@42393:                  " ((rhs (1 = 2 * (1 + -1 * sqrt x))) is_sqrtTerm_in x)");
neuper@42393: val SOME (t, _) = rewrite_set_ thy true rooteq_srls t;
neuper@42393: term2str t = "True | True"; (*...was same in 2002 (NOT "True"); so program seems to take 
neuper@42393:   [univariate,equation] and to refine to ["sq", "root'", "univariate", "equation"] in 2002*)
neuper@42393: 
neuper@42393: (*(*these are the errors during stepping into the code:*)
neuper@42393: nxt_solve_ (pt,ip); (*check_elementwise: no set 1 = 2 + -2 * sqrt x: fun mk_set raises
neuper@42393:   this exn in Check_elementwise ONLY ?!?*)
neuper@42393: step p ((pt, e_pos'),[]); (* = ("helpless",*)
neuper@42393: *)
neuper@42393: 
neuper@42393: val (p,_,f,nxt,_,pt) = me nxt p''' c pt''';
neuper@42393: f2str f = "1 = 2 + -2 * sqrt x)"; (* <<<-------------- this should be*)
neuper@42393: fst nxt = "Empty_Tac"; (* <<<-------------- this we have*)
neuper@42393: (*============ inhibit exn WN120314: stopped due to effort; continue with equ-solver
neuper@42393: The equation is strange: it calls script ["RootEq","solve_sq_root_equation"] twice
neuper@42393: and works differently due to an "if" in that script.
neuper@42393: 
neuper@42393: if f2str f = "1 = 2 + -2 * sqrt x" then ()
neuper@42393: else error "rootrateq.sml: diff.behav. in rootrat_equation_left_1 b";
neuper@42393: (*-> Subproblem ("RootRatEq", ["sq", "root'", "univariate", "equation"]) ?!? the SAME as above*)
neuper@42393: val (p,_,f,nxt,_,pt) = me nxt p c pt; 
neuper@42393: val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
neuper@42393: val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f; 
neuper@42393: val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
neuper@42393: val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f; 
neuper@42393: val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
neuper@42393: val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f; 
neuper@42393: val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
neuper@42393: val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
neuper@42393: val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
neuper@42393: val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
neuper@42393: if f2str f = "1 = 4 * x" then ()
neuper@42393: else error "rootrateq.sml: diff.behav. in rootrat_equation_left_1 c";
neuper@42393: (*-> Subproblem ("PolyEq", ["normalize", "polynomial", "univariate", "equation"])*)
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p c pt; 
neuper@42393: if f2str f = "1 + -4 * x = 0" then ()
neuper@38031: else error "rootrateq.sml: diff.behav. in rootrat_equation_left_1";
neuper@42393: (*-> Subproblem ("PolyEq", ["degree_1", "polynomial", "univariate", "equation"])*)
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
neuper@37906: case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 1 / 4]")) => ()
neuper@38031: 	 | _ => error "rootrateq.sml: diff.behav. in  -2 + 1/(1 - sqrt(x))= 0 -> [x = 1/4]";
neuper@42393: ============ inhibit exn WN120314 ==============================================*)
neuper@42398: ============ inhibit exn WN120319 ==============================================*)
neuper@37906: 
neuper@42393: "------------ test thm rootrat_equation_left_2 -------------------";
neuper@42393: "------------ test thm rootrat_equation_left_2 -------------------";
neuper@42393: "------------ test thm rootrat_equation_left_2 -------------------";
neuper@37906: val fmz = ["equality (3/(1+sqrt(x))= 1)", "solveFor x","solutions L"];
neuper@37991: val (dI',pI',mI') = ("RootRatEq",["univariate","equation"],["no_met"]);
neuper@37906: 
neuper@37906: val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p c pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
neuper@37991: (*-> Subproblem ("RootEq", ["univariate", ...])*)
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p c pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p c pt; 
neuper@37991: (*-> Subproblem ("RootEq", ["univariate", ...])*)
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p c pt; 
neuper@37991: (*-> Subproblem ("RootEq", ["univariate", ...])*)
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p c pt; 
neuper@42393: (*============ inhibit exn WN120314 ==============================================
neuper@37906: if f = Form' (FormKF (~1, EdUndef, 0, Nundef, "4 + -1 * x = 0")) then ()
neuper@38031: else error "rootrateq.sml: diff.behav. in rootrat_equation_left_2";
neuper@37991: (*-> Subproblem ("PolyEq", ["polynomial", ...])*)
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
neuper@37906: case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 4]")) => ()
neuper@38031: 	 | _ => error "rootrateq.sml: diff.behav. in  3/(1+sqrt(x))= 1 -> [x = 4]";
neuper@42393: ============ inhibit exn WN120314 ==============================================*)
neuper@37906: 
neuper@42393: "------------ test thm rootrat_equation_right_1 ------------------";
neuper@42393: "------------ test thm rootrat_equation_right_1 ------------------";
neuper@42393: "------------ test thm rootrat_equation_right_1 ------------------";
neuper@37906: val fmz = ["equality ( 0= -2 + 1/(1 - sqrt(x)))", "solveFor x","solutions L"];
neuper@37991: val (dI',pI',mI') = ("RootRatEq",["univariate","equation"],["no_met"]);
neuper@37906: 
neuper@37906: val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p c pt; 
neuper@42393: (*============ inhibit exn WN120314: similar complicated equation, dropped.
neuper@37906: if f = Form' (FormKF (~1, EdUndef, 0, Nundef, "-1 + 4 * x = 0")) then ()
neuper@38031: else error "rootrateq.sml: diff.behav.ppoly in rootrat_equation_right_1";
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p c pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
neuper@37906: case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 1 / 4]")) => ()
neuper@38031: 	 | _ => error "rootrateq.sml: diff.behav. in  -2 + 1/(1 - sqrt(x))= 0 -> [x = 1/4]";
neuper@42393: ============ inhibit exn WN120314 ==============================================*)
neuper@37906: 
neuper@42393: "------------ test thm rootrat_equation_right_2 ------------------";
neuper@42393: "------------ test thm rootrat_equation_right_2 ------------------";
neuper@42393: "------------ test thm rootrat_equation_right_2 ------------------";
neuper@37906: val fmz = ["equality (1 = 3/(1+sqrt(x)))", "solveFor x","solutions L"];
neuper@37991: val (dI',pI',mI') = ("RootRatEq",["univariate","equation"],["no_met"]);
neuper@37906: 
neuper@37906: val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p c pt; 
neuper@42393: (*============ inhibit exn WN120314 ==============================================
neuper@37906: if f = Form' (FormKF (~1, EdUndef, 0, Nundef, "-4 + x = 0")) then ()
neuper@38031: else error "rootrateq.sml: diff.behav. in rootrat_equation_right_2";
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p c pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
neuper@37906: case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 4]")) => ()
neuper@38031: 	 | _ => error "rootrateq.sml: diff.behav. in  3/(1+sqrt(x))= 1 -> [x = 4]";
neuper@42393: ============ inhibit exn WN120314 ==============================================*)
neuper@42393: