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

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

author	Walther Neuper <neuper@ist.tugraz.at>
	Wed, 08 Sep 2010 16:47:22 +0200
branch	isac-update-Isa09-2
changeset 37991	028442673981
parent 37960	ec20007095f2
child 38031	460c24a6a6ba
permissions	-rw-r--r--