wneuper/isa: test/Tools/isac/Knowledge/polyeq.sml@b95f0dde56c1 (annotated)

neuper@37906	1	(* testexamples for PolyEq, poynomial equations and equational systems
neuper@42248	2	author: Richard Lang 2003
neuper@37906	3	(c) due to copyright terms
neuper@37906	4	WN030609: some expls dont work due to unfinished handling of 'expanded terms';
neuper@37906	5	others marked with TODO have to be checked, too.
neuper@37906	6	*)
neuper@37906	7
neuper@37906	8	"-----------------------------------------------------------------";
neuper@37906	9	"table of contents -----------------------------------------------";
neuper@37906	10	(WN060608 some ----- are not in this table)
neuper@37906	11	"-----------------------------------------------------------------";
neuper@37906	12	"----------- tests on predicates in problems ---------------------";
neuper@37906	13	"----------- test matching problems --------------------------0---";
neuper@42248	14	"----------- lin.eq degree_0 -------------------------------------";
neuper@42248	15	"----------- test thm's d2_pq_formulsxx[_neg]---------------------";
neuper@37906	16	"----------- (-8 - 2x + x^^^2 = 0), (Schalk 2, S.67 Nr.31.b----";
neuper@37906	17	"----------- (-16 + 4x + 2x^^^2 = 0), --------------------------";
neuper@37906	18	"----------- (ab - (a+b)x + x^^^2 = 0), (Schalk 2,S.68Nr.44.a)";
neuper@37906	19	"----------- (-64 + x^^^2 = 0), (Schalk 2, S.66 Nr.1.a~--------)";
neuper@37906	20	"----------- (-147 + 3x^^^2 = 0), (Schalk 2, S.66 Nr.1.b------*)";
neuper@37906	21	"----------- (3x - 1 - (5x - (2 - 4x)) = -11),(Schalk Is86Bsp5";
neuper@37906	22	"----------- ((x+1)(x+2) - (3x - 2)^^^2=.. Schalk II s.68 Bsp 37";
neuper@37906	23	"----------- interSteps ([1],Res); on Schalk Is86Bsp5-------------";
neuper@37906	24	"-----------------------------------------------------------------";
neuper@37906	25	"-----------------------------------------------------------------";
neuper@37906	26	"-----------------------------------------------------------------";
neuper@37906	27
neuper@37906	28	"----------- tests on predicates in problems ---------------------";
neuper@37906	29	"----------- tests on predicates in problems ---------------------";
neuper@37906	30	"----------- tests on predicates in problems ---------------------";
neuper@37906	31	(*
neuper@37906	32	trace_rewrite:=true;
neuper@37906	33	trace_rewrite:=false;
neuper@37906	34	*)
neuper@37906	35	val t1 = (term_of o the o (parse thy)) "lhs (-8 - 2*x + x^^^2 = 0)";
neuper@42248	36	val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t1;
neuper@37906	37	if ((term2str t) = "-8 - 2 * x + x ^^^ 2") then ()
neuper@38031	38	else error "polyeq.sml: diff.behav. in lhs";
neuper@37906	39
neuper@37906	40	val t2 = (term_of o the o (parse thy)) "(-8 - 2*x + x^^^2) is_expanded_in x";
neuper@42248	41	val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t2;
neuper@42248	42	if (term2str t) = "True" then ()
neuper@38031	43	else error "polyeq.sml: diff.behav. 1 in is_expended_in";
neuper@37906	44
neuper@37906	45	val t0 = (term_of o the o (parse thy)) "(sqrt(x)) is_poly_in x";
neuper@42248	46	val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t0;
neuper@42248	47	if (term2str t) = "False" then ()
neuper@38031	48	else error "polyeq.sml: diff.behav. 2 in is_poly_in";
neuper@37906	49
neuper@37906	50	val t3 = (term_of o the o (parse thy)) "(-8 + (-1)2x + x^^^2) is_poly_in x";
neuper@42248	51	val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t3;
neuper@42248	52	if (term2str t) = "True" then ()
neuper@38031	53	else error "polyeq.sml: diff.behav. 3 in is_poly_in";
neuper@37906	54
neuper@37906	55	val t4 = (term_of o the o (parse thy)) "(lhs (-8 + (-1)2x + x^^^2 = 0)) is_expanded_in x";
neuper@42248	56	val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t4;
neuper@42248	57	if (term2str t) = "True" then ()
neuper@38031	58	else error "polyeq.sml: diff.behav. 4 in is_expended_in";
neuper@37906	59
neuper@37906	60
neuper@37906	61	val t6 = (term_of o the o (parse thy)) "(lhs (-8 - 2*x + x^^^2 = 0)) is_expanded_in x";
neuper@42248	62	val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t6;
neuper@42248	63	if (term2str t) = "True" then ()
neuper@38031	64	else error "polyeq.sml: diff.behav. 5 in is_expended_in";
neuper@37906	65
neuper@37906	66	val t3 = (term_of o the o (parse thy))"((-8 - 2*x + x^^^2) has_degree_in x) = 2";
neuper@42248	67	val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t3;
neuper@42248	68	if (term2str t) = "True" then ()
neuper@38031	69	else error "polyeq.sml: diff.behav. in has_degree_in_in";
neuper@37906	70
neuper@37906	71	val t3 = (term_of o the o (parse thy)) "((sqrt(x)) has_degree_in x) = 2";
neuper@42248	72	val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t3;
neuper@42248	73	if (term2str t) = "False" then ()
neuper@38031	74	else error "polyeq.sml: diff.behav. 6 in has_degree_in_in";
neuper@37906	75
neuper@37906	76	val t4 = (term_of o the o (parse thy))
neuper@37906	77	"((-8 - 2*x + x^^^2) has_degree_in x) = 1";
neuper@42248	78	val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t4;
neuper@42248	79	if (term2str t) = "False" then ()
neuper@38031	80	else error "polyeq.sml: diff.behav. 7 in has_degree_in_in";
neuper@37906	81
neuper@37906	82	val t5 = (term_of o the o (parse thy))
neuper@37906	83	"((-8 - 2*x + x^^^2) has_degree_in x) = 2";
neuper@42248	84	val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t5;
neuper@42248	85	if (term2str t) = "True" then ()
neuper@38031	86	else error "polyeq.sml: diff.behav. 8 in has_degree_in_in";
neuper@37906	87
neuper@42248	88	"----------- test matching problems --------------------------0---";
neuper@42248	89	"----------- test matching problems --------------------------0---";
neuper@42248	90	"----------- test matching problems --------------------------0---";
neuper@42248	91	val fmz = ["equality (-8 - 2*x + x^^^2 = 0)", "solveFor x","solutions L"];
neuper@42248	92	if match_pbl fmz (get_pbt ["expanded","univariate","equation"]) =
neuper@42248	93	Matches' {Find = [Correct "solutions L"],
neuper@42248	94	With = [],
neuper@42248	95	Given = [Correct "equality (-8 - 2 * x + x ^^^ 2 = 0)", Correct "solveFor x"],
neuper@42248	96	Where = [Correct "matches (?a = 0) (-8 - 2 * x + x ^^^ 2 = 0)",
neuper@42248	97	Correct "lhs (-8 - 2 * x + x ^^^ 2 = 0) is_expanded_in x"],
neuper@42248	98	Relate = []}
neuper@42248	99	then () else error "match_pbl [expanded,univariate,equation]";
neuper@37906	100
neuper@42248	101	if match_pbl fmz (get_pbt ["degree_2","expanded","univariate","equation"]) =
neuper@42248	102	Matches' {Find = [Correct "solutions L"],
neuper@42248	103	With = [],
neuper@42248	104	Given = [Correct "equality (-8 - 2 * x + x ^^^ 2 = 0)", Correct "solveFor x"],
neuper@42248	105	Where = [Correct "lhs (-8 - 2 * x + x ^^^ 2 = 0) has_degree_in x = 2"],
neuper@42248	106	Relate = []} (before WN110906 was: has_degree_in x =!= 2"])
neuper@42248	107	then () else error "match_pbl [degree_2,expanded,univariate,equation]";
neuper@37906	108
neuper@42248	109	"----------- lin.eq degree_0 -------------------------------------";
neuper@42248	110	"----------- lin.eq degree_0 -------------------------------------";
neuper@42248	111	"----------- lin.eq degree_0 -------------------------------------";
neuper@37906	112	"----- d0_false ------";
neuper@42248	113	val fmz = ["equality (1 = (0::real))", "solveFor x", "solutions L"];
neuper@37991	114	val (dI',pI',mI') = ("PolyEq",["degree_0","polynomial","univariate","equation"],
neuper@37906	115	["PolyEq","solve_d0_polyeq_equation"]);
neuper@42283	116	(*=== inhibit exn WN110914: declare_constraints doesnt work with num_str ========
neuper@42283	117	TODO: change to "equality (x + -1*x = (0::real))"
neuper@42283	118	and search for an appropriate problem and method.
neuper@42283	119
neuper@37906	120	val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
neuper@42272	121	val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	122	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	123	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	124	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	125	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	126	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@37906	127	case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[]")) => ()
neuper@38031	128	\| _ => error "polyeq.sml: diff.behav. in 1 = 0 -> []";
neuper@37906	129
neuper@37906	130	"----- d0_true ------";
neuper@42248	131	val fmz = ["equality (0 = (0::real))", "solveFor x","solutions L"];
neuper@37991	132	val (dI',pI',mI') = ("PolyEq",["degree_0","polynomial","univariate","equation"],
neuper@37906	133	["PolyEq","solve_d0_polyeq_equation"]);
neuper@37906	134	val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
neuper@42272	135	val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	136	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	137	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	138	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	139	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	140	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@37906	141	case f of Form' (FormKF (~1,EdUndef,0,Nundef,"UniversalList")) => ()
neuper@38031	142	\| _ => error "polyeq.sml: diff.behav. in 0 = 0 -> UniversalList";
neuper@42272	143	============ inhibit exn WN110914 ============================================*)
neuper@37906	144
neuper@42248	145	"----------- test thm's d2_pq_formulsxx[_neg]---------------------";
neuper@42248	146	"----------- test thm's d2_pq_formulsxx[_neg]---------------------";
neuper@42248	147	"----------- test thm's d2_pq_formulsxx[_neg]---------------------";
neuper@37906	148	"----- d2_pqformula1 ------!!!!";
neuper@42255	149	val fmz = ["equality (-1/8 + (-1/4)*z + z^^^2 = (0::real))", "solveFor z","solutions L"];
neuper@42255	150	val (dI',pI',mI') =
neuper@42255	151	("Isac", ["pqFormula","degree_2","polynomial","univariate","equation"], ["no_met"]);
neuper@37906	152	val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
neuper@42255	153	val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42255	154	val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42255	155	val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42255	156	val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42255	157	val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42255	158	val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42255	159	val (p,_,f,nxt,_,pt) = me nxt p [] pt; (Apply_Method ["PolyEq", "solve_d2_polyeq_pq_equation"])
neuper@42255	160	val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42255	161	val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42255	162	val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42255	163	val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42255	164	([z = 1 / 8 + sqrt (9 / 16) / 2, z = 1 / 8 + -1 sqrt (9 / 16) / 2] TODO sqrt*)
neuper@42255	165	val (p,_,f,nxt,_,pt) = me nxt p [] pt; (nxt =..,Check_elementwise "Assumptions"))
neuper@42255	166	"~~~~~ fun me, args:"; val ((_,tac), (p:pos'), _, (pt:ptree)) = (nxt, p, [], pt);
neuper@42255	167	"~~~~~ fun locatetac, args:"; val (tac, (ptp as (pt, p))) = (tac, (pt, p));
neuper@42255	168	val (mI,m) = mk_tac'_ tac;
neuper@42255	169	val Appl m = applicable_in p pt m;
neuper@42255	170	val Check_elementwise' (trm1, str, (trm2, trms)) = m;
neuper@42255	171	term2str trm1 = "[z = 1 / 8 + sqrt (9 / 16) / 2, z = 1 / 8 + -1 * sqrt (9 / 16) / 2]";
neuper@42255	172	str = "Assumptions";
neuper@42255	173	term2str trm2 = "[z = 1 / 8 + sqrt (9 / 16) / 2, z = 1 / 8 + -1 * sqrt (9 / 16) / 2]";
neuper@42255	174	terms2str trms = "[\"lhs (-1 / 8 + -1 * (1 / 8 + sqrt (9 / 16) / 2) / 4 +\n "^
neuper@42255	175	" (1 / 8 + sqrt (9 / 16) / 2) ^^^ 2 =\n 0) is_poly_in 1 / 8 + sqrt (9 / 16) / 2\","^
neuper@42255	176	"\"lhs (-1 / 8 + -1 * (1 / 8 + sqrt (9 / 16) / 2) / 4 +\n (1 / 8 + sqrt (9 / 16) / 2) ^^^ 2 =\n 0) "^
neuper@42255	177	"has_degree_in 1 / 8 + sqrt (9 / 16) / 2 =\n2\","^
neuper@42255	178	"\"lhs (-1 / 8 + -1 * (1 / 8 + -1 * sqrt (9 / 16) / 2) / 4 +\n (1 / 8 + -1 * sqrt (9 / 16) / 2) ^^^ 2 =\n 0) is_poly_in 1 / 8 + -1 * sqrt (9 / 16) / 2\","^
neuper@42255	179	"\"lhs (-1 / 8 + -1 * (1 / 8 + -1 * sqrt (9 / 16) / 2) / 4 +\n (1 / 8 + -1 * sqrt (9 / 16) / 2) ^^^ 2 =\n 0) has_degree_in 1 / 8 + -1 * sqrt (9 / 16) / 2 =\n2\"]";
neuper@42255	180	(TODO simplify assumptions (sqrt!) and check ERROR in has_degree_in);
neuper@42255	181	member op = specsteps mI (false);
neuper@42255	182	(*loc_solve_ (mI,m) ptp;
neuper@42255	183	WAS: not-found-in-script: NotLocatable from NasNap (Const ("List...*)
neuper@42255	184	"~~~~~ fun loc_solve_, args:"; val (m, (pt,pos)) = ((mI,m), ptp);
neuper@42255	185	(*solve m (pt, pos);
neuper@42255	186	WAS: not-found-in-script: NotLocatable from NasNap (Const ("List...*)
neuper@42255	187	"~~~~~ fun solve, args:"; val ((mI,m), (pt, po as (p,p_))) = (m, (pt, pos));
neuper@42255	188	e_metID = get_obj g_metID pt (par_pblobj pt p) (false);
neuper@42255	189	val thy' = get_obj g_domID pt (par_pblobj pt p);
neuper@42255	190	val (srls, is, sc) = from_pblobj_or_detail' thy' (p,p_) pt;
neuper@42255	191	val d = e_rls;
neuper@42255	192	(*locate_gen (thy',srls) m (pt,(p,p_)) (sc,d) is;
neuper@42255	193	WAS: not-found-in-script: NotLocatable from NasNap (Const ("List...*)
neuper@42255	194	"~~~~~ fun locate_gen, args:"; val ((ts as (thy',srls)), (m:tac_), ((pt,p):ptree * pos'),
neuper@42255	195	(scr as Script (h $ body),d), (ScrState (E,l,a,v,S,b), ctxt)) =
neuper@42255	196	((thy',srls), m ,(pt,(p,p_)) ,(sc,d) ,is); (* locate_gen 2nd pattern *)
neuper@42255	197	val thy = assoc_thy thy';
neuper@42255	198	l = [] orelse ((last_elem o fst) p = 0 andalso snd p = Res) (false);
neuper@42255	199	(*WAS val NasApp _ =(astep_up (thy',srls,scr,d) ((E,l,a,v,S,b), [(m,EmptyMout,pt,p,[])]) )
neuper@42255	200	... Assoc ... is correct*)
neuper@42255	201	"~~~~~ and astep_up, args:"; val ((ys as (_,_,Script sc,_)), ((E,l,a,v,S,b),ss)) =
neuper@42255	202	((thy',srls,scr,d), ((E,l,a,v,S,b), [(m,EmptyMout,pt,p,[])]));
neuper@42255	203	1 < length l (true);
neuper@42255	204	val up = drop_last l;
neuper@42255	205	term2str (go up sc);
neuper@42255	206	(go up sc);
neuper@42255	207	(*WAS val NasNap _ = ass_up ys ((E,up,a,v,S,b),ss) (go up sc)
neuper@42255	208	... ???? ... is correct*)
neuper@42255	209	"~~~~~ fun ass_up, args:"; val ((ys as (y,s,Script sc,d)), (is as (E,l,a,v,S,b),ss),
neuper@42255	210	(Const ("HOL.Let",_) $ _)) = (ys, ((E,up,a,v,S,b),ss), (go up sc));
neuper@42255	211	val l = drop_last l; (comes from e, goes to Abs)
neuper@42255	212	val (Const ("HOL.Let",_) $ e $ (Abs (i,T,body))) = go l sc;
neuper@42255	213	val i = mk_Free (i, T);
neuper@42255	214	val E = upd_env E (i, v);
neuper@42255	215	(Type error ...: Can't unify _a to pos pos_ (Incompatible types)*)
neuper@42255	216	val [(tac_, mout, ptree, pos', xxx)] = ss;
neuper@42255	217	val ss = [(tac_, mout, ptree, pos', []:(pos * pos_) list)];
neuper@42255	218	(*WAS val NasApp iss = assy (((y,s),d),Aundef) ((E, l@[R,D], a,v,S,b),ss) body
neuper@42255	219	... Assoc ... is correct*)
neuper@42255	220	"~~~~~ fun assy, args:"; val ((((thy',sr),d),ap), (is as (E,l,a,v,S,b), (m,_,pt,(p,p_),c)::ss), t) =
neuper@42255	221	((((y,s),d),Aundef), ((E, l@[R,D], a,v,S,b),ss), body);
neuper@42255	222	val (a', STac stac) = handle_leaf "locate" thy' sr E a v t
neuper@42255	223	val ctxt = get_ctxt pt (p,p_)
neuper@42255	224	val p' = lev_on p : pos;
neuper@42255	225	(* WAS val NotAss = assod pt d m stac
neuper@42255	226	... Ass ... is correct*)
neuper@42255	227	"~~~~~ fun assod, args:"; val (pt, _, (m as Check_elementwise' (consts,_,(consts_chkd,_))),
neuper@42255	228	(Const ("Script.Check'_elementwise",_) $ consts' $ _)) = (pt, d, m, stac);
neuper@42255	229	term2str consts;
neuper@42255	230	term2str consts';
neuper@42255	231	if consts = consts' (WAS false) then () else error "Check_elementwise changed";
neuper@42260	232	([z = 1 / 8 + sqrt (9 / 16) / 2, z = 1 / 8 + -1 sqrt (9 / 16) / 2] TODO sqrt*)
neuper@42272	233	*}
neuper@42272	234
neuper@42272	235
neuper@42272	236	ML {*
neuper@37906	237
neuper@37906	238	"----- d2_pqformula1_neg ------";
neuper@42272	239	val fmz = ["equality (2 +(-1)*x + x^^^2 = (0::real))", "solveFor x","solutions L"];
neuper@37991	240	val (dI',pI',mI') = ("PolyEq",["pqFormula","degree_2","polynomial","univariate","equation"], ["PolyEq","solve_d2_polyeq_pq_equation"]);
neuper@37906	241	val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
neuper@42272	242	val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	243	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	244	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	245	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	246	*}
neuper@42272	247	ML {*
neuper@42272	248	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@37906	249	(*### or2list False
neuper@37906	250	([1],Res) False Or_to_List)*)
neuper@42272	251	val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@37906	252	(*### or2list False
neuper@37906	253	([2],Res) [] Check_elementwise "Assumptions"*)
neuper@42272	254	val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	255	val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@37906	256	val asm = get_assumptions_ pt p;
neuper@37906	257	if f = Form' (FormKF (~1,EdUndef,0,Nundef,"[]")) andalso asm = [] then ()
neuper@38031	258	else error "polyeq.sml: diff.behav. in 2 +(-1)*x + x^^^2 = 0";
neuper@42272	259	*}
neuper@42272	260	ML {*
neuper@37906	261
neuper@37906	262	"----- d2_pqformula2 ------";
neuper@37906	263	val fmz = ["equality (-2 +(-1)x + 1x^^^2 = 0)", "solveFor x","solutions L"];
neuper@37991	264	val (dI',pI',mI') = ("PolyEq",["pqFormula","degree_2","polynomial","univariate","equation"],
neuper@37906	265	["PolyEq","solve_d2_polyeq_pq_equation"]);
neuper@42272	266	(*val p = e_pos';
neuper@37906	267	val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
neuper@42272	268	val (p,_,f,nxt,_,pt) = me (mI,m) p [] EmptyPtree;*)
neuper@37906	269	val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
neuper@42272	270	val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	271	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	272	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	273	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	274	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	275	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	276	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	277	val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@37906	278	case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 2, x = -1]")) => ()
neuper@38031	279	\| _ => error "polyeq.sml: diff.behav. in -2 + (-1)*x + x^2 = 0 -> [x = 2, x = -1]";
neuper@37906	280
neuper@37906	281
neuper@37906	282	"----- d2_pqformula2_neg ------";
neuper@37906	283	val fmz = ["equality ( 2 +(-1)x + 1x^^^2 = 0)", "solveFor x","solutions L"];
neuper@37991	284	val (dI',pI',mI') = ("PolyEq",["pqFormula","degree_2","polynomial","univariate","equation"],
neuper@37906	285	["PolyEq","solve_d2_polyeq_pq_equation"]);
neuper@37906	286	(*val p = e_pos'; val c = [];
neuper@37906	287	val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
neuper@37906	288	val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
neuper@37906	289	val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
neuper@42272	290	val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	291	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	292	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	293	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	294	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	295	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	296	val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@37906	297	"TODO 2 +(-1)x + 1x^^^2 = 0";
neuper@37906	298	"TODO 2 +(-1)x + 1x^^^2 = 0";
neuper@37906	299	"TODO 2 +(-1)x + 1x^^^2 = 0";
neuper@37906	300
neuper@37906	301
neuper@37906	302	"----- d2_pqformula3 ------";
neuper@37906	303	(EP-9)
neuper@37906	304	val fmz = ["equality (-2 + x + x^^^2 = 0)", "solveFor x","solutions L"];
neuper@37991	305	val (dI',pI',mI') = ("PolyEq",["pqFormula","degree_2","polynomial","univariate","equation"],
neuper@37906	306	["PolyEq","solve_d2_polyeq_pq_equation"]);
neuper@37906	307	(*val p = e_pos'; val c = [];
neuper@37906	308	val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
neuper@37906	309	val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
neuper@37906	310	val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
neuper@42272	311	val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	312	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	313	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	314	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	315	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	316	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	317	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	318	val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@37906	319	case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 1, x = -2]")) => ()
neuper@38031	320	\| _ => error "polyeq.sml: diff.behav. in -2 + x + x^2 = 0-> [x = 1, x = -2]";
neuper@37906	321
neuper@37906	322	"----- d2_pqformula3_neg ------";
neuper@37906	323	val fmz = ["equality ( 2 + x + x^^^2 = 0)", "solveFor x","solutions L"];
neuper@37991	324	val (dI',pI',mI') = ("PolyEq",["pqFormula","degree_2","polynomial","univariate","equation"],
neuper@37906	325	["PolyEq","solve_d2_polyeq_pq_equation"]);
neuper@37906	326	(*val p = e_pos'; val c = [];
neuper@37906	327	val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
neuper@37906	328	val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
neuper@37906	329	val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
neuper@42272	330	val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	331	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	332	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	333	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	334	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	335	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	336	val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@37906	337	"TODO 2 + x + x^^^2 = 0";
neuper@37906	338	"TODO 2 + x + x^^^2 = 0";
neuper@37906	339	"TODO 2 + x + x^^^2 = 0";
neuper@37906	340
neuper@37906	341
neuper@37906	342	"----- d2_pqformula4 ------";
neuper@37906	343	val fmz = ["equality (-2 + x + 1*x^^^2 = 0)", "solveFor x","solutions L"];
neuper@37991	344	val (dI',pI',mI') = ("PolyEq",["pqFormula","degree_2","polynomial","univariate","equation"],
neuper@37906	345	["PolyEq","solve_d2_polyeq_pq_equation"]);
neuper@37906	346	(*val p = e_pos'; val c = [];
neuper@37906	347	val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
neuper@37906	348	val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
neuper@37906	349	val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
neuper@42272	350	val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	351	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	352	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	353	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	354	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	355	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	356	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	357	val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@37906	358	case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 1, x = -2]")) => ()
neuper@38031	359	\| _ => error "polyeq.sml: diff.behav. in -2 + x + 1*x^^^2 = 0 -> [x = 1, x = -2]";
neuper@37906	360
neuper@37906	361	"----- d2_pqformula4_neg ------";
neuper@37906	362	val fmz = ["equality ( 2 + x + 1*x^^^2 = 0)", "solveFor x","solutions L"];
neuper@37991	363	val (dI',pI',mI') = ("PolyEq",["pqFormula","degree_2","polynomial","univariate","equation"],
neuper@37906	364	["PolyEq","solve_d2_polyeq_pq_equation"]);
neuper@37906	365	(*val p = e_pos'; val c = [];
neuper@37906	366	val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
neuper@37906	367	val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
neuper@37906	368	val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
neuper@42272	369	val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	370	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	371	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	372	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	373	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	374	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@37906	375	"TODO 2 + x + 1*x^^^2 = 0";
neuper@37906	376	"TODO 2 + x + 1*x^^^2 = 0";
neuper@37906	377	"TODO 2 + x + 1*x^^^2 = 0";
neuper@37906	378
neuper@37906	379	"----- d2_pqformula5 ------";
neuper@37906	380	val fmz = ["equality (1*x + x^^^2 = 0)", "solveFor x","solutions L"];
neuper@37991	381	val (dI',pI',mI') = ("PolyEq",["pqFormula","degree_2","polynomial","univariate","equation"],
neuper@37906	382	["PolyEq","solve_d2_polyeq_pq_equation"]);
neuper@37906	383	(*val p = e_pos'; val c = [];
neuper@37906	384	val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
neuper@37906	385	val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
neuper@37906	386	val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
neuper@42272	387	val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	388	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	389	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	390	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	391	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	392	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	393	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	394	val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@37906	395	case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 0, x = -1]")) => ()
neuper@38031	396	\| _ => error "polyeq.sml: diff.behav. in 1*x + x^2 = 0 -> [x = 0, x = -1]";
neuper@37906	397
neuper@37906	398	"----- d2_pqformula6 ------";
neuper@37906	399	val fmz = ["equality (1x + 1x^^^2 = 0)", "solveFor x","solutions L"];
neuper@37991	400	val (dI',pI',mI') = ("PolyEq",["pqFormula","degree_2","polynomial","univariate","equation"],
neuper@37906	401	["PolyEq","solve_d2_polyeq_pq_equation"]);
neuper@37906	402	(*val p = e_pos'; val c = [];
neuper@37906	403	val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
neuper@37906	404	val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
neuper@37906	405	val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
neuper@42272	406	val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	407	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	408	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	409	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	410	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	411	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	412	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	413	val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@37906	414	case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 0, x = -1]")) => ()
neuper@38031	415	\| _ => error "polyeq.sml: diff.behav. in 1x + 1x^2 = 0 -> [x = 0, x = -1]";
neuper@37906	416
neuper@37906	417	"----- d2_pqformula7 ------";
neuper@37906	418	(EP-10)
neuper@37906	419	val fmz = ["equality ( x + x^^^2 = 0)", "solveFor x","solutions L"];
neuper@37991	420	val (dI',pI',mI') = ("PolyEq",["pqFormula","degree_2","polynomial","univariate","equation"],
neuper@37906	421	["PolyEq","solve_d2_polyeq_pq_equation"]);
neuper@37906	422	(*val p = e_pos'; val c = [];
neuper@37906	423	val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
neuper@37906	424	val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
neuper@37906	425	val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
neuper@42272	426	val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	427	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	428	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	429	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	430	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	431	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	432	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	433	val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@37906	434	case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 0, x = -1]")) => ()
neuper@38031	435	\| _ => error "polyeq.sml: diff.behav. in x + x^2 = 0 -> [x = 0, x = -1]";
neuper@37906	436
neuper@37906	437	"----- d2_pqformula8 ------";
neuper@37906	438	val fmz = ["equality ( x + 1*x^^^2 = 0)", "solveFor x","solutions L"];
neuper@37991	439	val (dI',pI',mI') = ("PolyEq",["pqFormula","degree_2","polynomial","univariate","equation"],
neuper@37906	440	["PolyEq","solve_d2_polyeq_pq_equation"]);
neuper@37906	441	(*val p = e_pos'; val c = [];
neuper@37906	442	val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
neuper@37906	443	val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
neuper@37906	444
neuper@37906	445	val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
neuper@42272	446	val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	447	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	448	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	449	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	450	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	451	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	452	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	453	val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@37906	454	case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 0, x = -1]")) => ()
neuper@38031	455	\| _ => error "polyeq.sml: diff.behav. in x + 1*x^2 = 0 -> [x = 0, x = -1]";
neuper@37906	456
neuper@37906	457	"----- d2_pqformula9 ------";
neuper@37906	458	val fmz = ["equality (-4 + x^^^2 = 0)", "solveFor x","solutions L"];
neuper@37991	459	val (dI',pI',mI') = ("PolyEq",["pqFormula","degree_2","polynomial","univariate","equation"],
neuper@37906	460	["PolyEq","solve_d2_polyeq_pq_equation"]);
neuper@37906	461	(*val p = e_pos'; val c = [];
neuper@37906	462	val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
neuper@37906	463	val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
neuper@37906	464
neuper@37906	465	val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
neuper@42272	466	val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	467	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	468	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	469	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	470	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	471	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	472	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@37906	473	case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 2, x = -2]")) => ()
neuper@38031	474	\| _ => error "polyeq.sml: diff.behav. in -4 + x^2 = 0 -> [x = 2, x = -2]";
neuper@37906	475
neuper@37906	476
neuper@37906	477	"----- d2_pqformula10_neg ------";
neuper@37906	478	val fmz = ["equality (4 + x^^^2 = 0)", "solveFor x","solutions L"];
neuper@37991	479	val (dI',pI',mI') = ("PolyEq",["pqFormula","degree_2","polynomial","univariate","equation"],
neuper@37906	480	["PolyEq","solve_d2_polyeq_pq_equation"]);
neuper@37906	481	(*val p = e_pos'; val c = [];
neuper@37906	482	val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
neuper@37906	483	val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
neuper@37906	484
neuper@37906	485	val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
neuper@42272	486	val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	487	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	488	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	489	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	490	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	491	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	492	val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@37906	493	"TODO 4 + x^^^2 = 0";
neuper@37906	494	"TODO 4 + x^^^2 = 0";
neuper@37906	495	"TODO 4 + x^^^2 = 0";
neuper@37906	496
neuper@37906	497	"----- d2_pqformula10 ------";
neuper@37906	498	val fmz = ["equality (-4 + 1*x^^^2 = 0)", "solveFor x","solutions L"];
neuper@37991	499	val (dI',pI',mI') = ("PolyEq",["pqFormula","degree_2","polynomial","univariate","equation"],
neuper@37906	500	["PolyEq","solve_d2_polyeq_pq_equation"]);
neuper@37906	501	(*val p = e_pos'; val c = [];
neuper@37906	502	val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
neuper@37906	503	val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
neuper@37906	504
neuper@37906	505	val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
neuper@42272	506	val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	507	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	508	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	509	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	510	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	511	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	512	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@37906	513	case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 2, x = -2]")) => ()
neuper@38031	514	\| _ => error "polyeq.sml: diff.behav. in -4 + 1*x^2 = 0 -> [x = 2, x = -2]";
neuper@37906	515
neuper@37906	516	"----- d2_pqformula9_neg ------";
neuper@37906	517	val fmz = ["equality (4 + 1*x^^^2 = 0)", "solveFor x","solutions L"];
neuper@37991	518	val (dI',pI',mI') = ("PolyEq",["pqFormula","degree_2","polynomial","univariate","equation"],
neuper@37906	519	["PolyEq","solve_d2_polyeq_pq_equation"]);
neuper@37906	520	(*val p = e_pos'; val c = [];
neuper@37906	521	val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
neuper@37906	522	val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
neuper@37906	523
neuper@37906	524	val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
neuper@42272	525	val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	526	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	527	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	528	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	529	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	530	val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@37906	531	"TODO 4 + 1*x^^^2 = 0";
neuper@37906	532	"TODO 4 + 1*x^^^2 = 0";
neuper@37906	533	"TODO 4 + 1*x^^^2 = 0";
neuper@37906	534
neuper@37906	535	"-------------------- test thm's d2_abc_formulsxx[_neg]-----";
neuper@37906	536	"-------------------- test thm's d2_abc_formulsxx[_neg]-----";
neuper@37906	537	"-------------------- test thm's d2_abc_formulsxx[_neg]-----";
neuper@37906	538
neuper@37906	539	val fmz = ["equality (-1 +(-1)x + 2x^^^2 = 0)", "solveFor x","solutions L"];
neuper@37991	540	val (dI',pI',mI') = ("PolyEq",["abcFormula","degree_2","polynomial","univariate","equation"],
neuper@37906	541	["PolyEq","solve_d2_polyeq_abc_equation"]);
neuper@37906	542	(*val p = e_pos'; val c = [];
neuper@37906	543	val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
neuper@37906	544	val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
neuper@37906	545
neuper@37906	546	val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
neuper@42272	547	val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	548	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	549	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	550	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	551	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	552	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	553	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@37906	554	case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 1, x = -1 / 2]")) => ()
neuper@38031	555	\| _ => error "polyeq.sml: diff.behav. in -1 + (-1)x + 2x^2 = 0 -> [x = 1, x = -1/2]";
neuper@37906	556
neuper@37906	557	val fmz = ["equality ( 1 +(-1)x + 2x^^^2 = 0)", "solveFor x","solutions L"];
neuper@37991	558	val (dI',pI',mI') = ("PolyEq",["abcFormula","degree_2","polynomial","univariate","equation"],
neuper@37906	559	["PolyEq","solve_d2_polyeq_abc_equation"]);
neuper@37906	560	(*val p = e_pos'; val c = [];
neuper@37906	561	val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
neuper@37906	562	val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
neuper@37906	563
neuper@37906	564	val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
neuper@42272	565	val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	566	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	567	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	568	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	569	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	570	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@37906	571	"TODO 1 +(-1)x + 2x^^^2 = 0";
neuper@37906	572	"TODO 1 +(-1)x + 2x^^^2 = 0";
neuper@37906	573	"TODO 1 +(-1)x + 2x^^^2 = 0";
neuper@37906	574
neuper@37906	575	(EP-11)
neuper@37906	576	val fmz = ["equality (-1 + x + 2*x^^^2 = 0)", "solveFor x","solutions L"];
neuper@37991	577	val (dI',pI',mI') = ("PolyEq",["abcFormula","degree_2","polynomial","univariate","equation"],
neuper@37906	578	["PolyEq","solve_d2_polyeq_abc_equation"]);
neuper@37906	579	(*val p = e_pos'; val c = [];
neuper@37906	580	val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
neuper@37906	581	val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
neuper@37906	582
neuper@37906	583	val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
neuper@42272	584	val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	585	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	586	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	587	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	588	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	589	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	590	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@37906	591	case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 1 / 2, x = -1]")) => ()
neuper@38031	592	\| _ => error "polyeq.sml: diff.behav. in -1 + x + 2*x^2 = 0 -> [x = 1/2, x = -1]";
neuper@37906	593
neuper@37906	594	val fmz = ["equality ( 1 + x + 2*x^^^2 = 0)", "solveFor x","solutions L"];
neuper@37991	595	val (dI',pI',mI') = ("PolyEq",["abcFormula","degree_2","polynomial","univariate","equation"],
neuper@37906	596	["PolyEq","solve_d2_polyeq_abc_equation"]);
neuper@37906	597	(*val p = e_pos'; val c = [];
neuper@37906	598	val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
neuper@37906	599	val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
neuper@37906	600
neuper@37906	601	val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
neuper@42272	602	val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	603	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	604	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	605	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	606	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	607	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	608	val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@37906	609	"TODO 1 + x + 2*x^^^2 = 0";
neuper@37906	610	"TODO 1 + x + 2*x^^^2 = 0";
neuper@37906	611	"TODO 1 + x + 2*x^^^2 = 0";
neuper@37906	612
neuper@37906	613	val fmz = ["equality (-2 + 1*x + x^^^2 = 0)", "solveFor x","solutions L"];
neuper@37991	614	val (dI',pI',mI') = ("PolyEq",["abcFormula","degree_2","polynomial","univariate","equation"],
neuper@37906	615	["PolyEq","solve_d2_polyeq_abc_equation"]);
neuper@37906	616	(*val p = e_pos'; val c = [];
neuper@37906	617	val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
neuper@37906	618	val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
neuper@37906	619
neuper@37906	620	val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
neuper@42272	621	val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	622	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	623	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	624	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	625	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	626	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	627	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@37906	628	case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 1, x = -2]")) => ()
neuper@38031	629	\| _ => error "polyeq.sml: diff.behav. in -2 + 1*x + x^2 = 0 -> [x = 1, x = -2]";
neuper@37906	630
neuper@37906	631	val fmz = ["equality ( 2 + 1*x + x^^^2 = 0)", "solveFor x","solutions L"];
neuper@37991	632	val (dI',pI',mI') = ("PolyEq",["abcFormula","degree_2","polynomial","univariate","equation"],
neuper@37906	633	["PolyEq","solve_d2_polyeq_abc_equation"]);
neuper@37906	634	(*val p = e_pos'; val c = [];
neuper@37906	635	val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
neuper@37906	636	val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
neuper@37906	637
neuper@37906	638	val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
neuper@42272	639	val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	640	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	641	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	642	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	643	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	644	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	645	val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@37906	646	"TODO 2 + 1*x + x^^^2 = 0";
neuper@37906	647	"TODO 2 + 1*x + x^^^2 = 0";
neuper@37906	648	"TODO 2 + 1*x + x^^^2 = 0";
neuper@37906	649
neuper@37906	650	(EP-12)
neuper@37906	651	val fmz = ["equality (-2 + x + x^^^2 = 0)", "solveFor x","solutions L"];
neuper@37991	652	val (dI',pI',mI') = ("PolyEq",["abcFormula","degree_2","polynomial","univariate","equation"],
neuper@37906	653	["PolyEq","solve_d2_polyeq_abc_equation"]);
neuper@37906	654	(*val p = e_pos'; val c = [];
neuper@37906	655	val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
neuper@37906	656	val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
neuper@37906	657
neuper@37906	658	val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
neuper@42272	659	val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	660	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	661	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	662	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	663	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	664	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	665	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@37906	666	case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 1, x = -2]")) => ()
neuper@38031	667	\| _ => error "polyeq.sml: diff.behav. in -2 + x + x^2 = 0 -> [x = 1, x = -2]";
neuper@37906	668
neuper@37906	669	val fmz = ["equality ( 2 + x + x^^^2 = 0)", "solveFor x","solutions L"];
neuper@37991	670	val (dI',pI',mI') = ("PolyEq",["abcFormula","degree_2","polynomial","univariate","equation"],
neuper@37906	671	["PolyEq","solve_d2_polyeq_abc_equation"]);
neuper@37906	672	(*val p = e_pos'; val c = [];
neuper@37906	673	val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
neuper@37906	674	val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
neuper@37906	675
neuper@37906	676	val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
neuper@42272	677	val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	678	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	679	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	680	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	681	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	682	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	683	val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@37906	684	"TODO 2 + x + x^^^2 = 0";
neuper@37906	685	"TODO 2 + x + x^^^2 = 0";
neuper@37906	686	"TODO 2 + x + x^^^2 = 0";
neuper@37906	687
neuper@37906	688	(EP-13)
neuper@37906	689	val fmz = ["equality (-8 + 2*x^^^2 = 0)", "solveFor x","solutions L"];
neuper@37991	690	val (dI',pI',mI') = ("PolyEq",["abcFormula","degree_2","polynomial","univariate","equation"],
neuper@37906	691	["PolyEq","solve_d2_polyeq_abc_equation"]);
neuper@37906	692	(*val p = e_pos'; val c = [];
neuper@37906	693	val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
neuper@37906	694	val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
neuper@37906	695
neuper@37906	696	val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
neuper@42272	697	val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	698	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	699	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	700	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	701	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	702	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	703	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@37906	704	case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 2, x = -2]")) => ()
neuper@38031	705	\| _ => error "polyeq.sml: diff.behav. in -8 + 2*x^2 = 0 -> [x = 2, x = -2]";
neuper@37906	706
neuper@37906	707	val fmz = ["equality ( 8+ 2*x^^^2 = 0)", "solveFor x","solutions L"];
neuper@37991	708	val (dI',pI',mI') = ("PolyEq",["abcFormula","degree_2","polynomial","univariate","equation"],
neuper@37906	709	["PolyEq","solve_d2_polyeq_abc_equation"]);
neuper@37906	710	(*val p = e_pos'; val c = [];
neuper@37906	711	val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
neuper@37906	712	val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
neuper@37906	713
neuper@37906	714	val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
neuper@42272	715	val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	716	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	717	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	718	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	719	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	720	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@37906	721	"TODO 8+ 2*x^^^2 = 0";
neuper@37906	722	"TODO 8+ 2*x^^^2 = 0";
neuper@37906	723	"TODO 8+ 2*x^^^2 = 0";
neuper@37906	724
neuper@37906	725	(EP-14)
neuper@37906	726	val fmz = ["equality (-4 + x^^^2 = 0)", "solveFor x","solutions L"];
neuper@37991	727	val (dI',pI',mI') = ("PolyEq",["abcFormula","degree_2","polynomial","univariate","equation"], ["PolyEq","solve_d2_polyeq_abc_equation"]);
neuper@37906	728	(*val p = e_pos'; val c = [];
neuper@37906	729	val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
neuper@37906	730	val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
neuper@37906	731
neuper@37906	732	val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
neuper@42272	733	val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	734	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	735	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	736	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	737	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	738	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	739	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@37906	740	case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 2, x = -2]")) => ()
neuper@38031	741	\| _ => error "polyeq.sml: diff.behav. in -4 + x^2 = 0 -> [x = 2, x = -2]";
neuper@37906	742
neuper@37906	743
neuper@37906	744	val fmz = ["equality ( 4+ x^^^2 = 0)", "solveFor x","solutions L"];
neuper@37991	745	val (dI',pI',mI') = ("PolyEq",["abcFormula","degree_2","polynomial","univariate","equation"], ["PolyEq","solve_d2_polyeq_abc_equation"]);
neuper@37906	746	(*val p = e_pos'; val c = [];
neuper@37906	747	val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
neuper@37906	748	val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
neuper@37906	749
neuper@37906	750	val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
neuper@42272	751	val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	752	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	753	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	754	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	755	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	756	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@37906	757	"TODO 4+ x^^^2 = 0";
neuper@37906	758	"TODO 4+ x^^^2 = 0";
neuper@37906	759	"TODO 4+ x^^^2 = 0";
neuper@37906	760
neuper@37906	761	(EP-15)
neuper@37906	762	val fmz = ["equality (2x + 2x^^^2 = 0)", "solveFor x","solutions L"];
neuper@37991	763	val (dI',pI',mI') = ("PolyEq",["abcFormula","degree_2","polynomial","univariate","equation"],
neuper@37906	764	["PolyEq","solve_d2_polyeq_abc_equation"]);
neuper@37906	765	(*val p = e_pos'; val c = [];
neuper@37906	766	val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
neuper@37906	767	val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
neuper@37906	768
neuper@37906	769	val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
neuper@42272	770	val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	771	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	772	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	773	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	774	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	775	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	776	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@37906	777	case f of Form' (FormKF (~1,EdUndef,_,Nundef,"[x = 0, x = -1]")) => ()
neuper@38031	778	\| _ => error "polyeq.sml: diff.behav. in x + x^2 = 0 -> [x = 0, x = -1]";
neuper@37906	779
neuper@37906	780	val fmz = ["equality (1*x + x^^^2 = 0)", "solveFor x","solutions L"];
neuper@37991	781	val (dI',pI',mI') = ("PolyEq",["abcFormula","degree_2","polynomial","univariate","equation"],
neuper@37906	782	["PolyEq","solve_d2_polyeq_abc_equation"]);
neuper@37906	783	(*val p = e_pos'; val c = [];
neuper@37906	784	val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
neuper@37906	785	val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
neuper@37906	786
neuper@37906	787	val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
neuper@42272	788	val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	789	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	790	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	791	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	792	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	793	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	794	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@37906	795	case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 0, x = -1]")) => ()
neuper@38031	796	\| _ => error "polyeq.sml: diff.behav. in x + x^2 = 0 -> [x = 0, x = -1]";
neuper@37906	797
neuper@37906	798	(EP-16)
neuper@37906	799	val fmz = ["equality (x + 2*x^^^2 = 0)", "solveFor x","solutions L"];
neuper@37991	800	val (dI',pI',mI') = ("PolyEq",["abcFormula","degree_2","polynomial","univariate","equation"],
neuper@37906	801	["PolyEq","solve_d2_polyeq_abc_equation"]);
neuper@37906	802	(*val p = e_pos'; val c = [];
neuper@37906	803	val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
neuper@37906	804	val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
neuper@37906	805
neuper@37906	806	val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
neuper@42272	807	val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	808	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	809	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	810	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	811	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	812	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	813	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@37906	814	case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 0, x = -1 / 2]")) => ()
neuper@38031	815	\| _ => error "polyeq.sml: diff.behav. in x + x^2 = 0 -> [x = 0, x = -1 / 2]";
neuper@37906	816
neuper@37906	817	(EP-//)
neuper@37906	818	val fmz = ["equality (x + x^^^2 = 0)", "solveFor x","solutions L"];
neuper@37991	819	val (dI',pI',mI') = ("PolyEq",["abcFormula","degree_2","polynomial","univariate","equation"],
neuper@37906	820	["PolyEq","solve_d2_polyeq_abc_equation"]);
neuper@37906	821	(*val p = e_pos'; val c = [];
neuper@37906	822	val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
neuper@37906	823	val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
neuper@37906	824
neuper@37906	825	val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
neuper@42272	826	val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	827	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	828	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	829	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	830	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	831	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	832	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@37906	833	case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 0, x = -1]")) => ()
neuper@38031	834	\| _ => error "polyeq.sml: diff.behav. in x + x^2 = 0 -> [x = 0, x = -1]";
neuper@37906	835
neuper@37906	836	"----------- (-8 - 2x + x^^^2 = 0), (Schalk 2, S.67 Nr.31.b----";
neuper@37906	837	"----------- (-8 - 2x + x^^^2 = 0), (Schalk 2, S.67 Nr.31.b----";
neuper@37906	838	"----------- (-8 - 2x + x^^^2 = 0), (Schalk 2, S.67 Nr.31.b----";
neuper@37906	839	val fmz = ["equality (-8 - 2x + x^^^2 = 0)", (Schalk 2, S.67 Nr.31.b*)
neuper@37906	840	"solveFor x","solutions L"];
neuper@37906	841	val (dI',pI',mI') =
neuper@37991	842	("PolyEq",["degree_2","expanded","univariate","equation"],
neuper@37906	843	["PolyEq","complete_square"]);
neuper@37906	844	(* val p = e_pos'; val c = [];
neuper@37906	845	val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
neuper@37906	846	val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
neuper@37906	847
neuper@37906	848	val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
neuper@42272	849	val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	850	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	851	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	852	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@37991	853	(Apply_Method ("PolyEq","complete_square"))
neuper@42272	854	val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@37906	855	("-8 - 2 x + x ^^^ 2 = 0", nxt = Rewrite_Set_Inst ... "complete_square*)
neuper@42272	856	val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@37906	857	("-8 + (2 / 2 - x) ^^^ 2 = (2 / 2) ^^^ 2", nxt = Rewrite("square_explicit1")
neuper@42272	858	val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@37906	859	("(2 / 2 - x) ^^^ 2 = (2 / 2) ^^^ 2 - -8" nxt = Rewrite("root_plus_minus)
neuper@42272	860	val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@37906	861	(*"2 / 2 - x = sqrt ((2 / 2) ^^^ 2 - -8) \|
neuper@37906	862	2 / 2 - x = - sqrt ((2 / 2) ^^^ 2 - -8)" nxt = Rewr_Inst("bdv_explicit2"*)
neuper@42272	863	val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@37906	864	(*"2 / 2 - x = sqrt ((2 / 2) ^^^ 2 - -8) \|
neuper@37906	865	-1x = - (2 / 2) + - sqrt ((2 / 2) ^^^ 2 - -8)"nxt = R_Inst("bdv_explt2")
neuper@42272	866	val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@37906	867	("-1 x = - (2 / 2) + sqrt ((2 / 2) ^^^ 2 - -8) \|
neuper@37906	868	-1 * x = (- (2 / 2) + - sqrt ((2 / 2) ^^^ 2 - -8))"nxt = bdv_explicit3*)
neuper@42272	869	val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@37906	870	("-1 x = - (2 / 2) + sqrt ((2 / 2) ^^^ 2 - -8) \|
neuper@37906	871	x = -1 * (- (2 / 2) + - sqrt ((2 / 2) ^^^ 2 - -8))" nxt = bdv_explicit3*)
neuper@42272	872	val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@37906	873	("x = -1 (- (2 / 2) + sqrt ((2 / 2) ^^^ 2 - -8)) \|
neuper@37906	874	x = -1 * (- (2 / 2) + - sqrt ((2 / 2) ^^^ 2 - -8))"nxt = calculate_Ration*)
neuper@42272	875	val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@37906	876	("x = -2 \| x = 4" nxt = Or_to_List)
neuper@42272	877	val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@37906	878	("[x = -2, x = 4]" nxt = Check_Postcond)
neuper@42272	879	val (p,_,f,nxt,_,pt) = me nxt p [] pt; f2str f;
neuper@37906	880	(* FIXXXME
neuper@37906	881	case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = -2, x = 4]")) => () TODO
neuper@38031	882	\| _ => error "polyeq.sml: diff.behav. in [x = -2, x = 4]";
neuper@37906	883	*)
neuper@37906	884	if f2str f = "[x = -1 * -1 + -1 * sqrt (1 ^^^ 2 - -8),\n x = -1 * -1 + -1 * (-1 * sqrt (1 ^^^ 2 - -8))]" then ()
neuper@38031	885	else error "polyeq.sml corrected?behav. in [x = -2, x = 4]";
neuper@37906	886
neuper@37906	887
neuper@37906	888	"-------------------- (3 - 10x + 3x^^^2 = 0), ----------------------";
neuper@37906	889	"-------------------- (3 - 10x + 3x^^^2 = 0), ----------------------";
neuper@37906	890	"-------------------- (3 - 10x + 3x^^^2 = 0), ----------------------";
neuper@37906	891	"---- test the erls ----";
neuper@37906	892	val t1 = (term_of o the o (parse thy)) "0 <= (10/3/2)^^^2 - 1";
neuper@37926	893	val SOME (t,_) = rewrite_set_ PolyEq.thy false PolyEq_erls t1;
neuper@37906	894	val t' = term2str t;
neuper@41928	895	(*if t'= "HOL.True" then ()
neuper@38031	896	else error "polyeq.sml: diff.behav. in 'rewrite_set_.. PolyEq_erls";*)
neuper@37906	897	(* *)
neuper@37906	898	val fmz = ["equality (3 - 10x + 3x^^^2 = 0)",
neuper@37906	899	"solveFor x","solutions L"];
neuper@37906	900	val (dI',pI',mI') =
neuper@37991	901	("PolyEq",["degree_2","expanded","univariate","equation"],
neuper@37906	902	["PolyEq","complete_square"]);
neuper@37906	903	(* val p = e_pos'; val c = [];
neuper@37906	904	val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
neuper@37906	905	val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
neuper@37906	906
neuper@37906	907	val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
neuper@42272	908	val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	909	val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	910	val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	911	val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	912	val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	913	val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	914	val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@37991	915	(Apply_Method ("PolyEq","complete_square"))
neuper@42272	916	val (p,_,f,nxt,_,pt) = me nxt p [] pt; f2str f;
neuper@37906	917
neuper@37906	918	"----------- (-16 + 4x + 2x^^^2 = 0), --------------------------";
neuper@37906	919	"----------- (-16 + 4x + 2x^^^2 = 0), --------------------------";
neuper@37906	920	"----------- (-16 + 4x + 2x^^^2 = 0), --------------------------";
neuper@37906	921	val fmz = ["equality (-16 + 4x + 2x^^^2 = 0)",
neuper@37906	922	"solveFor x","solutions L"];
neuper@37906	923	val (dI',pI',mI') =
neuper@37991	924	("PolyEq",["degree_2","expanded","univariate","equation"],
neuper@37906	925	["PolyEq","complete_square"]);
neuper@37906	926	(* val p = e_pos'; val c = [];
neuper@37906	927	val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
neuper@37906	928	val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
neuper@37906	929
neuper@37906	930	val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
neuper@42272	931	val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	932	val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	933	val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	934	val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	935	val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	936	val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	937	val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@37991	938	(Apply_Method ("PolyEq","complete_square"))
neuper@42272	939	val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	940	val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	941	val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	942	val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	943	val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	944	val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	945	val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	946	val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	947	val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	948	val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@37906	949	(* FIXXXXME n1.,
neuper@37906	950	case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 2, x = -4]")) => () TODO
neuper@38031	951	\| _ => error "polyeq.sml: diff.behav. in [x = 2, x = -4]";
neuper@37906	952	*)
neuper@37906	953
neuper@37906	954	"----------- (ab - (a+b)x + x^^^2 = 0), (Schalk 2,S.68Nr.44.a)";
neuper@37906	955	"----------- (ab - (a+b)x + x^^^2 = 0), (Schalk 2,S.68Nr.44.a)";
neuper@37906	956	"----------- (ab - (a+b)x + x^^^2 = 0), (Schalk 2,S.68Nr.44.a)";
neuper@37906	957	val fmz = ["equality (ab - (a+b)x + x^^^2 = 0)",
neuper@37906	958	"solveFor x","solutions L"];
neuper@37906	959	val (dI',pI',mI') =
neuper@37991	960	("PolyEq",["degree_2","expanded","univariate","equation"],
neuper@37906	961	["PolyEq","complete_square"]);
neuper@37906	962	(* val p = e_pos'; val c = [];
neuper@37906	963	val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
neuper@37906	964	val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
neuper@37906	965
neuper@37906	966	val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
neuper@42272	967	val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	968	val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	969	val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	970	val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	971	val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	972	val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	973	val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	974	val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	975	val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	976	val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@37906	977
neuper@42272	978	val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	979	val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	980	val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	981	val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	982	val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	983	val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	984	val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	985	val (p,_,f,nxt,_,pt) = me nxt p [] pt; f2str f;
neuper@37906	986	(*WN.2.5.03 TODO FIXME Matthias ?
neuper@37906	987	case f of
neuper@37906	988	Form'
neuper@37906	989	(FormKF
neuper@37906	990	(~1,EdUndef,0,Nundef,
neuper@37906	991	"[x = (a + b) / 2 + -1 * sqrt ((a + b) ^^^ 2 / 2 ^^^ 2 - a * b),\n x = (a + b) / 2 + sqrt ((a + b) ^^^ 2 / 2 ^^^ 2 - a * b)]"))
neuper@37906	992	=> ()
neuper@38031	993	\| _ => error "polyeq.sml: diff.behav. in ab - (a+b)x + x^^^2 = 0";
neuper@37906	994	this will be simplified [x = a, x = b] to by Factor.ML*)
neuper@37906	995
neuper@37906	996
neuper@37906	997	"----------- (-64 + x^^^2 = 0), (Schalk 2, S.66 Nr.1.a~--------)";
neuper@37906	998	"----------- (-64 + x^^^2 = 0), (Schalk 2, S.66 Nr.1.a~--------)";
neuper@37906	999	"----------- (-64 + x^^^2 = 0), (Schalk 2, S.66 Nr.1.a~--------)";
neuper@37906	1000	val fmz = ["equality (-64 + x^^^2 = 0)",(Schalk 2, S.66 Nr.1.a~)
neuper@37906	1001	"solveFor x","solutions L"];
neuper@37906	1002	val (dI',pI',mI') =
neuper@37991	1003	("PolyEq",["degree_2","expanded","univariate","equation"],
neuper@37906	1004	["PolyEq","complete_square"]);
neuper@37906	1005	(* val p = e_pos'; val c = [];
neuper@37906	1006	val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
neuper@37906	1007	val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
neuper@37906	1008
neuper@37906	1009	val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
neuper@42272	1010	val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	1011	val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	1012	val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	1013	val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	1014	val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	1015	val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	1016	val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	1017	val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	1018	val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	1019	val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	1020	val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	1021	val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	1022	val (p,_,f,nxt,_,pt) = me nxt p [] pt; f2str f;
neuper@37906	1023	(WN.2.5.03 TODO "[x = sqrt (0 - -64), x = -1 sqrt (0 - -64)]"
neuper@37906	1024	case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 8, x = -8]")) => ()
neuper@38031	1025	\| _ => error "polyeq.sml: diff.behav. in [x = 8, x = -8]";
neuper@37906	1026	*)
neuper@37906	1027
neuper@37906	1028	"----------- (-147 + 3x^^^2 = 0), (Schalk 2, S.66 Nr.1.b------*)";
neuper@37906	1029	"----------- (-147 + 3x^^^2 = 0), (Schalk 2, S.66 Nr.1.b------*)";
neuper@37906	1030	"----------- (-147 + 3x^^^2 = 0), (Schalk 2, S.66 Nr.1.b------*)";
neuper@37906	1031	val fmz = ["equality (-147 + 3x^^^2 = 0)",(Schalk 2, S.66 Nr.1.b*)
neuper@37906	1032	"solveFor x","solutions L"];
neuper@37906	1033	val (dI',pI',mI') =
neuper@37991	1034	("PolyEq",["degree_2","expanded","univariate","equation"],
neuper@37906	1035	["PolyEq","complete_square"]);
neuper@37906	1036	(* val p = e_pos'; val c = [];
neuper@37906	1037	val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
neuper@37906	1038	val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
neuper@37906	1039
neuper@37906	1040	val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
neuper@42272	1041	val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	1042	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	1043	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	1044	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	1045	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	1046	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	1047	val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@42272	1048	val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@37906	1049	(WN.2.5.03 TODO "[x = sqrt (0 - -49), x = -1 sqrt (0 - -49)]"
neuper@37906	1050	case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 7, x = -7]")) => ()
neuper@38031	1051	\| _ => error "polyeq.sml: diff.behav. in [x = 7, x = -7]";
neuper@37906	1052	*)
neuper@37906	1053	if f2str f = "[x = sqrt (0 - -49), x = -1 * sqrt (0 - -49)]" then ()
neuper@38031	1054	else error "polyeq.sml CORRECTED?behav. in [x = 7, x = -7]";
neuper@37906	1055
neuper@37906	1056
neuper@37906	1057	"----------- (3x - 1 - (5x - (2 - 4x)) = -11),(Schalk Is86Bsp5";
neuper@37906	1058	"----------- (3x - 1 - (5x - (2 - 4x)) = -11),(Schalk Is86Bsp5";
neuper@37906	1059	"----------- (3x - 1 - (5x - (2 - 4x)) = -11),(Schalk Is86Bsp5";
neuper@37906	1060	(EP-17 Schalk_I_p86_n5)
neuper@37906	1061	val fmz = ["equality (3x - 1 - (5x - (2 - 4*x)) = -11)","solveFor x","solutions L"];
neuper@37906	1062	(* refine fmz ["univariate","equation"];
neuper@37906	1063	*)
neuper@37991	1064	val (dI',pI',mI') = ("PolyEq",["univariate","equation"],["no_met"]);
neuper@37906	1065	(*val p = e_pos';
neuper@37906	1066	val c = [];
neuper@37906	1067	val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
neuper@37906	1068	val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
neuper@37906	1069
neuper@37906	1070	val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
neuper@37906	1071	val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906	1072	(* val nxt =
neuper@37906	1073	("Model_Problem",
neuper@37906	1074	Model_Problem ["normalize","polynomial","univariate","equation"])
neuper@37906	1075	: string * tac*)
neuper@37906	1076	val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906	1077	val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906	1078	val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906	1079	val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906	1080	val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906	1081	(* val nxt =
neuper@37906	1082	("Subproblem",
neuper@37991	1083	Subproblem ("PolyEq",["polynomial","univariate","equation"]))
neuper@37906	1084	: string * tac *)
neuper@37906	1085	val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906	1086	(*val nxt =
neuper@37906	1087	("Model_Problem",
neuper@37906	1088	Model_Problem ["degree_1","polynomial","univariate","equation"])
neuper@37906	1089	: string * tac *)
neuper@37906	1090	val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906	1091	val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906	1092
neuper@37906	1093	val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906	1094	val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906	1095	val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906	1096	val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906	1097	val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906	1098	case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 2]")) => ()
neuper@38031	1099	\| _ => error "polyeq.sml: diff.behav. in [x = 2]";
neuper@37906	1100
neuper@37906	1101
neuper@37906	1102	"----------- ((x+1)(x+2) - (3x - 2)^^^2=.. Schalk II s.68 Bsp 37";
neuper@37906	1103	"----------- ((x+1)(x+2) - (3x - 2)^^^2=.. Schalk II s.68 Bsp 37";
neuper@37906	1104	"----------- ((x+1)(x+2) - (3x - 2)^^^2=.. Schalk II s.68 Bsp 37";
neuper@37906	1105	(is in rlang.sml, too)
neuper@37906	1106	val fmz = ["equality ((x+1)(x+2) - (3x - 2)^^^2=(2x - 1)^^^2+(3x - 1)*(x+1))",
neuper@37906	1107	"solveFor x","solutions L"];
neuper@37991	1108	val (dI',pI',mI') = ("PolyEq",["univariate","equation"],["no_met"]);
neuper@37906	1109
neuper@37906	1110	(*val p = e_pos'; val c = [];
neuper@37906	1111	val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
neuper@37906	1112	val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
neuper@37906	1113
neuper@37906	1114	val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
neuper@37906	1115	(val nxt = ("Refine_Tacitly",Refine_Tacitly ["univariate","equation"]))
neuper@37906	1116	val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906	1117	(* val nxt =
neuper@37906	1118	("Model_Problem",
neuper@37906	1119	Model_Problem ["normalize","polynomial","univariate","equation"])
neuper@37906	1120	: string * tac *)
neuper@37906	1121	val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906	1122	val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906	1123	val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906	1124	val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906	1125	val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906	1126	val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906	1127	(* val nxt =
neuper@37906	1128	("Subproblem",
neuper@37991	1129	Subproblem ("PolyEq",["polynomial","univariate","equation"]))
neuper@37906	1130	: string * tac*)
neuper@37906	1131	val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906	1132	(*val nxt =
neuper@37906	1133	("Model_Problem",
neuper@37906	1134	Model_Problem ["abcFormula","degree_2","polynomial","univariate","equation"])
neuper@37906	1135	: string * tac*)
neuper@37906	1136	val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906	1137	val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906	1138	val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906	1139	val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906	1140	val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906	1141	val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906	1142	val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906	1143	case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 2 / 15, x = 1]")) => ()
neuper@38031	1144	\| _ => error "polyeq.sml: diff.behav. in [x = 2 / 15, x = 1]";
neuper@37906	1145
neuper@37906	1146
neuper@37906	1147	" -4 + x^^^2 =0 ";
neuper@37906	1148	" -4 + x^^^2 =0 ";
neuper@37906	1149	" -4 + x^^^2 =0 ";
neuper@37906	1150	val fmz = ["equality ( -4 + x^^^2 =0)", "solveFor x","solutions L"];
neuper@37906	1151	(* val fmz = ["equality (1 + x^^^2 =0)", "solveFor x","solutions L"];*)
neuper@37906	1152	(val fmz = ["equality (0 =0)", "solveFor x","solutions L"];)
neuper@37991	1153	val (dI',pI',mI') = ("PolyEq",["univariate","equation"],["no_met"]);
neuper@37906	1154	(*val p = e_pos';
neuper@37906	1155	val c = [];
neuper@37906	1156	val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
neuper@37906	1157	val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
neuper@37906	1158	val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
neuper@37906	1159
neuper@37906	1160	val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906	1161	val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906	1162	val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906	1163	val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906	1164	val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906	1165	val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906	1166	val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906	1167	case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 2, x = -2]")) => ()
neuper@38031	1168	\| _ => error "polyeq.sml: diff.behav. in [x = 2, x = -2]";
neuper@37906	1169
neuper@37906	1170	"----------------- polyeq.sml end ------------------";
neuper@37906	1171
neuper@37906	1172	(Punkte aus dem TestBericht, die ich in rlang.sml nicht zuordnen konnte:)
neuper@37906	1173	(WN.19.3.03 ---v-)
neuper@37906	1174	(3(b))val (bdv,v) = (str2term "bdv", str2term "R1");
neuper@37906	1175	val t = str2term "-1 * (R * R2) + R2 * R1 + -1 * (R * R1) = 0";
neuper@37926	1176	val SOME (t',_) = rewrite_set_inst_ thy false [(bdv,v)] make_polynomial_in t;
neuper@37906	1177	term2str t';
neuper@37906	1178	"-1 * R * R2 + (R2 + -1 * R) * R1 = 0";
neuper@37906	1179	(WN.19.3.03 ---^-)
neuper@37906	1180
neuper@37906	1181	(3(c))val (bdv,v) = (str2term "bdv", str2term "p");
neuper@37906	1182	val t = str2term "y ^^^ 2 + -2 * (x * p) = 0";
neuper@37926	1183	val SOME (t',_) = rewrite_set_inst_ thy false [(bdv,v)] make_polynomial_in t;
neuper@37906	1184	term2str t';
neuper@37906	1185	"y ^^^ 2 + -2 * x * p = 0";
neuper@37906	1186
neuper@37906	1187	(3(d))val (bdv,v) = (str2term "bdv", str2term "x2");
neuper@37906	1188	val t = str2term
neuper@37906	1189	"A + x1 * (y3 * (1 / 2)) + x3 * (y2 * (1 / 2)) + -1 * (x1 * (y2 * (1 / 2))) + -1 * (x3 * (y1 * (1 / 2 ))) + y1 * (1 / 2 * x2) + -1 * (y3 * (1 / 2 * x2)) = 0";
neuper@37926	1190	val SOME (t',_) = rewrite_set_inst_ thy false [(bdv,v)] make_polynomial_in t;
neuper@37906	1191	term2str t';
neuper@37906	1192	"A + x1 * y3 * (1 / 2) + x3 * y2 * (1 / 2) + - x1 * y2 * (1 / 2) + - x3 * y1 * (1 / 2) + (y1 * (1 / 2) + - y3 * (1 / 2)) * x2 = 0";
neuper@37926	1193	val SOME (t',_) = rewrite_set_inst_ thy false [(bdv,v)] make_ratpoly_in t;
neuper@37906	1194	term2str t';
neuper@37906	1195	"A + x1 * y3 * (1 / 2) + x3 * y2 * (1 / 2) + -1 * x1 * y2 * (1 / 2) + -1 * x3 * y1 * (1 / 2) + (y1 * (1 / 2) + -1 * y3 * (1 / 2)) * x2 = 0";
neuper@37906	1196
neuper@37906	1197	(3(e))val (bdv,v) = (str2term "bdv", str2term "a");
neuper@37906	1198	val t = str2term
neuper@37906	1199	"A ^^^ 2 + c ^^^ 2 * (c / d) ^^^ 2 + (-4 * (c / d) ^^^ 2) * a ^^^ 2 = 0";
neuper@37926	1200	val NONE = rewrite_set_inst_ thy false [(bdv,v)] make_polynomial_in t;
neuper@37906	1201	(die _unsichtbare_ Klammern sind genau wie gew"unscht)
neuper@37906	1202
neuper@37906	1203
neuper@37906	1204	val t = str2term "(x + 1) * (x + 2) - (3 * x - 2) ^^^ 2 - ((2 * x - 1) ^^^ 2 + (3 * x - 1) * (x + 1)) = 0";
neuper@37906	1205	trace_rewrite:=true;
neuper@37906	1206	rewrite_set_ thy false expand_binoms t;
neuper@37906	1207	trace_rewrite:=false;
neuper@37906	1208
neuper@37906	1209
neuper@37906	1210	"----------- interSteps ([1],Res); on Schalk Is86Bsp5-------------";
neuper@37906	1211	"----------- interSteps ([1],Res); on Schalk Is86Bsp5-------------";
neuper@37906	1212	"----------- interSteps ([1],Res); on Schalk Is86Bsp5-------------";
neuper@37906	1213	states:=[];
neuper@37906	1214	CalcTree
neuper@37906	1215	[(["equality (3x - 1 - (5x - (2 - 4*x)) = -11)","solveFor x","solutions L"],
neuper@37991	1216	("PolyEq",["univariate","equation"],["no_met"]))];
neuper@37906	1217	Iterator 1;
neuper@37906	1218	moveActiveRoot 1;
neuper@37906	1219	autoCalculate 1 CompleteCalc;
neuper@37906	1220	val ((pt,p),_) = get_calc 1; show_pt pt;
neuper@37906	1221
neuper@37906	1222	interSteps 1 ([1],Res) (no Rewrite_Set...);
neuper@42248	1223
neuper@42248	1224	============ inhibit exn WN110906 ==============================================*)
neuper@42248	1225

author	Walther Neuper <neuper@ist.tugraz.at>
	Fri, 23 Sep 2011 13:58:27 +0200
branch	decompose-isar
changeset 42283	b95f0dde56c1
parent 42272	dcc5d2601cf7
child 42318	b4f9b188373e
permissions	-rw-r--r--