39 trace_rewrite:=false; |
39 trace_rewrite:=false; |
40 *) |
40 *) |
41 val t1 = (term_of o the o (parse thy)) "lhs (-8 - 2*x + x^^^2 = 0)"; |
41 val t1 = (term_of o the o (parse thy)) "lhs (-8 - 2*x + x^^^2 = 0)"; |
42 val SOME (t,_) = rewrite_set_ PolyEq.thy false PolyEq_prls t1; |
42 val SOME (t,_) = rewrite_set_ PolyEq.thy false PolyEq_prls t1; |
43 if ((term2str t) = "-8 - 2 * x + x ^^^ 2") then () |
43 if ((term2str t) = "-8 - 2 * x + x ^^^ 2") then () |
44 else raise error "polyeq.sml: diff.behav. in lhs"; |
44 else error "polyeq.sml: diff.behav. in lhs"; |
45 |
45 |
46 |
46 |
47 val t2 = (term_of o the o (parse thy)) "(-8 - 2*x + x^^^2) is_expanded_in x"; |
47 val t2 = (term_of o the o (parse thy)) "(-8 - 2*x + x^^^2) is_expanded_in x"; |
48 val SOME (t,_) = rewrite_set_ PolyEq.thy false PolyEq_prls t2; |
48 val SOME (t,_) = rewrite_set_ PolyEq.thy false PolyEq_prls t2; |
49 if (term2str t) = "True" then () |
49 if (term2str t) = "True" then () |
50 else raise error "polyeq.sml: diff.behav. 1 in is_expended_in"; |
50 else error "polyeq.sml: diff.behav. 1 in is_expended_in"; |
51 |
51 |
52 val t0 = (term_of o the o (parse thy)) "(sqrt(x)) is_poly_in x"; |
52 val t0 = (term_of o the o (parse thy)) "(sqrt(x)) is_poly_in x"; |
53 val SOME (t,_) = rewrite_set_ PolyEq.thy false PolyEq_prls t0; |
53 val SOME (t,_) = rewrite_set_ PolyEq.thy false PolyEq_prls t0; |
54 if (term2str t) = "False" then () |
54 if (term2str t) = "False" then () |
55 else raise error "polyeq.sml: diff.behav. 2 in is_poly_in"; |
55 else error "polyeq.sml: diff.behav. 2 in is_poly_in"; |
56 |
56 |
57 |
57 |
58 val t3 = (term_of o the o (parse thy)) "(-8 + (-1)*2*x + x^^^2) is_poly_in x"; |
58 val t3 = (term_of o the o (parse thy)) "(-8 + (-1)*2*x + x^^^2) is_poly_in x"; |
59 val SOME (t,_) = rewrite_set_ PolyEq.thy false PolyEq_prls t3; |
59 val SOME (t,_) = rewrite_set_ PolyEq.thy false PolyEq_prls t3; |
60 if (term2str t) = "True" then () |
60 if (term2str t) = "True" then () |
61 else raise error "polyeq.sml: diff.behav. 3 in is_poly_in"; |
61 else error "polyeq.sml: diff.behav. 3 in is_poly_in"; |
62 |
62 |
63 |
63 |
64 val t4 = (term_of o the o (parse thy)) "(lhs (-8 + (-1)*2*x + x^^^2 = 0)) is_expanded_in x"; |
64 val t4 = (term_of o the o (parse thy)) "(lhs (-8 + (-1)*2*x + x^^^2 = 0)) is_expanded_in x"; |
65 val SOME (t,_) = rewrite_set_ PolyEq.thy false PolyEq_prls t4; |
65 val SOME (t,_) = rewrite_set_ PolyEq.thy false PolyEq_prls t4; |
66 if (term2str t) = "True" then () |
66 if (term2str t) = "True" then () |
67 else raise error "polyeq.sml: diff.behav. 4 in is_expended_in"; |
67 else error "polyeq.sml: diff.behav. 4 in is_expended_in"; |
68 |
68 |
69 |
69 |
70 val t6 = (term_of o the o (parse thy)) "(lhs (-8 - 2*x + x^^^2 = 0)) is_expanded_in x"; |
70 val t6 = (term_of o the o (parse thy)) "(lhs (-8 - 2*x + x^^^2 = 0)) is_expanded_in x"; |
71 val SOME (t,_) = rewrite_set_ PolyEq.thy false PolyEq_prls t6; |
71 val SOME (t,_) = rewrite_set_ PolyEq.thy false PolyEq_prls t6; |
72 if (term2str t) = "True" then () |
72 if (term2str t) = "True" then () |
73 else raise error "polyeq.sml: diff.behav. 5 in is_expended_in"; |
73 else error "polyeq.sml: diff.behav. 5 in is_expended_in"; |
74 |
74 |
75 val t3 = (term_of o the o (parse thy))"((-8 - 2*x + x^^^2) has_degree_in x) = 2"; |
75 val t3 = (term_of o the o (parse thy))"((-8 - 2*x + x^^^2) has_degree_in x) = 2"; |
76 val SOME (t,_) = rewrite_set_ PolyEq.thy false PolyEq_prls t3; |
76 val SOME (t,_) = rewrite_set_ PolyEq.thy false PolyEq_prls t3; |
77 if (term2str t) = "True" then () |
77 if (term2str t) = "True" then () |
78 else raise error "polyeq.sml: diff.behav. in has_degree_in_in"; |
78 else error "polyeq.sml: diff.behav. in has_degree_in_in"; |
79 |
79 |
80 |
80 |
81 val t3 = (term_of o the o (parse thy)) "((sqrt(x)) has_degree_in x) = 2"; |
81 val t3 = (term_of o the o (parse thy)) "((sqrt(x)) has_degree_in x) = 2"; |
82 val SOME (t,_) = rewrite_set_ PolyEq.thy false PolyEq_prls t3; |
82 val SOME (t,_) = rewrite_set_ PolyEq.thy false PolyEq_prls t3; |
83 if (term2str t) = "False" then () |
83 if (term2str t) = "False" then () |
84 else raise error "polyeq.sml: diff.behav. 6 in has_degree_in_in"; |
84 else error "polyeq.sml: diff.behav. 6 in has_degree_in_in"; |
85 |
85 |
86 val t4 = (term_of o the o (parse thy)) |
86 val t4 = (term_of o the o (parse thy)) |
87 "((-8 - 2*x + x^^^2) has_degree_in x) = 1"; |
87 "((-8 - 2*x + x^^^2) has_degree_in x) = 1"; |
88 val SOME (t,_) = rewrite_set_ PolyEq.thy false PolyEq_prls t4; |
88 val SOME (t,_) = rewrite_set_ PolyEq.thy false PolyEq_prls t4; |
89 if (term2str t) = "False" then () |
89 if (term2str t) = "False" then () |
90 else raise error "polyeq.sml: diff.behav. 7 in has_degree_in_in"; |
90 else error "polyeq.sml: diff.behav. 7 in has_degree_in_in"; |
91 |
91 |
92 |
92 |
93 val t5 = (term_of o the o (parse thy)) |
93 val t5 = (term_of o the o (parse thy)) |
94 "((-8 - 2*x + x^^^2) has_degree_in x) = 2"; |
94 "((-8 - 2*x + x^^^2) has_degree_in x) = 2"; |
95 val SOME (t,_) = rewrite_set_ PolyEq.thy false PolyEq_prls t5; |
95 val SOME (t,_) = rewrite_set_ PolyEq.thy false PolyEq_prls t5; |
96 if (term2str t) = "True" then () |
96 if (term2str t) = "True" then () |
97 else raise error "polyeq.sml: diff.behav. 8 in has_degree_in_in"; |
97 else error "polyeq.sml: diff.behav. 8 in has_degree_in_in"; |
98 |
98 |
99 |
99 |
100 "----------- test matching problems --------------------------0---"; |
100 "----------- test matching problems --------------------------0---"; |
101 "----------- test matching problems --------------------------0---"; |
101 "----------- test matching problems --------------------------0---"; |
102 "----------- test matching problems --------------------------0---"; |
102 "----------- test matching problems --------------------------0---"; |
136 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; |
136 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; |
137 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; |
137 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; |
138 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; |
138 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; |
139 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; |
139 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; |
140 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[]")) => () |
140 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[]")) => () |
141 | _ => raise error "polyeq.sml: diff.behav. in 1 = 0 -> []"; |
141 | _ => error "polyeq.sml: diff.behav. in 1 = 0 -> []"; |
142 |
142 |
143 "----- d0_true ------"; |
143 "----- d0_true ------"; |
144 (*EP-7*) |
144 (*EP-7*) |
145 val fmz = ["equality ( 0 = 0)", "solveFor x","solutions L"]; |
145 val fmz = ["equality ( 0 = 0)", "solveFor x","solutions L"]; |
146 val (dI',pI',mI') = ("PolyEq",["degree_0","polynomial","univariate","equation"], |
146 val (dI',pI',mI') = ("PolyEq",["degree_0","polynomial","univariate","equation"], |
154 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; |
154 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; |
155 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; |
155 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; |
156 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; |
156 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; |
157 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; |
157 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; |
158 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"UniversalList")) => () |
158 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"UniversalList")) => () |
159 | _ => raise error "polyeq.sml: diff.behav. in 0 = 0 -> UniversalList"; |
159 | _ => error "polyeq.sml: diff.behav. in 0 = 0 -> UniversalList"; |
160 |
160 |
161 "-------------------- test thm's degree_2 ------------------------------------------"; |
161 "-------------------- test thm's degree_2 ------------------------------------------"; |
162 "-------------------- test thm's degree_2 ------------------------------------------"; |
162 "-------------------- test thm's degree_2 ------------------------------------------"; |
163 |
163 |
164 "-------------------- test thm's d2_pq_formulsxx[_neg]-----"; |
164 "-------------------- test thm's d2_pq_formulsxx[_neg]-----"; |
187 val (p,_,f,nxt,_,pt) = me nxt p c pt; |
187 val (p,_,f,nxt,_,pt) = me nxt p c pt; |
188 (*### applicable_in Check_elementwise: --> ([x = 2, x = -1], []) |
188 (*### applicable_in Check_elementwise: --> ([x = 2, x = -1], []) |
189 ([5],Res) "[x = 2, x = -1]" Check_Postcond*) |
189 ([5],Res) "[x = 2, x = -1]" Check_Postcond*) |
190 val (p,_,f,nxt,_,pt) = me nxt p c pt; |
190 val (p,_,f,nxt,_,pt) = me nxt p c pt; |
191 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 2, x = -1]")) => () |
191 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 2, x = -1]")) => () |
192 | _ => raise error "polyeq.sml: diff.behav. in -2 + (-1)*x + x^2 = 0 -> [x = 2, x = -1]"; |
192 | _ => error "polyeq.sml: diff.behav. in -2 + (-1)*x + x^2 = 0 -> [x = 2, x = -1]"; |
193 |
193 |
194 "----- d2_pqformula1_neg ------"; |
194 "----- d2_pqformula1_neg ------"; |
195 (*EP-8*) |
195 (*EP-8*) |
196 val fmz = ["equality ( 2 +(-1)*x + x^^^2 = 0)", "solveFor x","solutions L"]; |
196 val fmz = ["equality ( 2 +(-1)*x + x^^^2 = 0)", "solveFor x","solutions L"]; |
197 val (dI',pI',mI') = ("PolyEq",["pqFormula","degree_2","polynomial","univariate","equation"], ["PolyEq","solve_d2_polyeq_pq_equation"]); |
197 val (dI',pI',mI') = ("PolyEq",["pqFormula","degree_2","polynomial","univariate","equation"], ["PolyEq","solve_d2_polyeq_pq_equation"]); |
211 ([2],Res) [] Check_elementwise "Assumptions"*) |
211 ([2],Res) [] Check_elementwise "Assumptions"*) |
212 val (p,_,f,nxt,_,pt) = me nxt p c pt; |
212 val (p,_,f,nxt,_,pt) = me nxt p c pt; |
213 val (p,_,f,nxt,_,pt) = me nxt p c pt; |
213 val (p,_,f,nxt,_,pt) = me nxt p c pt; |
214 val asm = get_assumptions_ pt p; |
214 val asm = get_assumptions_ pt p; |
215 if f = Form' (FormKF (~1,EdUndef,0,Nundef,"[]")) andalso asm = [] then () |
215 if f = Form' (FormKF (~1,EdUndef,0,Nundef,"[]")) andalso asm = [] then () |
216 else raise error "polyeq.sml: diff.behav. in 2 +(-1)*x + x^^^2 = 0"; |
216 else error "polyeq.sml: diff.behav. in 2 +(-1)*x + x^^^2 = 0"; |
217 |
217 |
218 "----- d2_pqformula2 ------"; |
218 "----- d2_pqformula2 ------"; |
219 val fmz = ["equality (-2 +(-1)*x + 1*x^^^2 = 0)", "solveFor x","solutions L"]; |
219 val fmz = ["equality (-2 +(-1)*x + 1*x^^^2 = 0)", "solveFor x","solutions L"]; |
220 val (dI',pI',mI') = ("PolyEq",["pqFormula","degree_2","polynomial","univariate","equation"], |
220 val (dI',pI',mI') = ("PolyEq",["pqFormula","degree_2","polynomial","univariate","equation"], |
221 ["PolyEq","solve_d2_polyeq_pq_equation"]); |
221 ["PolyEq","solve_d2_polyeq_pq_equation"]); |
230 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; |
230 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; |
231 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; |
231 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; |
232 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; |
232 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; |
233 val (p,_,f,nxt,_,pt) = me nxt p c pt; |
233 val (p,_,f,nxt,_,pt) = me nxt p c pt; |
234 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 2, x = -1]")) => () |
234 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 2, x = -1]")) => () |
235 | _ => raise error "polyeq.sml: diff.behav. in -2 + (-1)*x + x^2 = 0 -> [x = 2, x = -1]"; |
235 | _ => error "polyeq.sml: diff.behav. in -2 + (-1)*x + x^2 = 0 -> [x = 2, x = -1]"; |
236 |
236 |
237 |
237 |
238 "----- d2_pqformula2_neg ------"; |
238 "----- d2_pqformula2_neg ------"; |
239 val fmz = ["equality ( 2 +(-1)*x + 1*x^^^2 = 0)", "solveFor x","solutions L"]; |
239 val fmz = ["equality ( 2 +(-1)*x + 1*x^^^2 = 0)", "solveFor x","solutions L"]; |
240 val (dI',pI',mI') = ("PolyEq",["pqFormula","degree_2","polynomial","univariate","equation"], |
240 val (dI',pI',mI') = ("PolyEq",["pqFormula","degree_2","polynomial","univariate","equation"], |
271 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; |
271 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; |
272 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; |
272 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; |
273 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; |
273 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; |
274 val (p,_,f,nxt,_,pt) = me nxt p c pt; |
274 val (p,_,f,nxt,_,pt) = me nxt p c pt; |
275 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 1, x = -2]")) => () |
275 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 1, x = -2]")) => () |
276 | _ => raise error "polyeq.sml: diff.behav. in -2 + x + x^2 = 0-> [x = 1, x = -2]"; |
276 | _ => error "polyeq.sml: diff.behav. in -2 + x + x^2 = 0-> [x = 1, x = -2]"; |
277 |
277 |
278 "----- d2_pqformula3_neg ------"; |
278 "----- d2_pqformula3_neg ------"; |
279 val fmz = ["equality ( 2 + x + x^^^2 = 0)", "solveFor x","solutions L"]; |
279 val fmz = ["equality ( 2 + x + x^^^2 = 0)", "solveFor x","solutions L"]; |
280 val (dI',pI',mI') = ("PolyEq",["pqFormula","degree_2","polynomial","univariate","equation"], |
280 val (dI',pI',mI') = ("PolyEq",["pqFormula","degree_2","polynomial","univariate","equation"], |
281 ["PolyEq","solve_d2_polyeq_pq_equation"]); |
281 ["PolyEq","solve_d2_polyeq_pq_equation"]); |
310 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; |
310 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; |
311 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; |
311 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; |
312 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; |
312 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; |
313 val (p,_,f,nxt,_,pt) = me nxt p c pt; |
313 val (p,_,f,nxt,_,pt) = me nxt p c pt; |
314 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 1, x = -2]")) => () |
314 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 1, x = -2]")) => () |
315 | _ => raise error "polyeq.sml: diff.behav. in -2 + x + 1*x^^^2 = 0 -> [x = 1, x = -2]"; |
315 | _ => error "polyeq.sml: diff.behav. in -2 + x + 1*x^^^2 = 0 -> [x = 1, x = -2]"; |
316 |
316 |
317 "----- d2_pqformula4_neg ------"; |
317 "----- d2_pqformula4_neg ------"; |
318 val fmz = ["equality ( 2 + x + 1*x^^^2 = 0)", "solveFor x","solutions L"]; |
318 val fmz = ["equality ( 2 + x + 1*x^^^2 = 0)", "solveFor x","solutions L"]; |
319 val (dI',pI',mI') = ("PolyEq",["pqFormula","degree_2","polynomial","univariate","equation"], |
319 val (dI',pI',mI') = ("PolyEq",["pqFormula","degree_2","polynomial","univariate","equation"], |
320 ["PolyEq","solve_d2_polyeq_pq_equation"]); |
320 ["PolyEq","solve_d2_polyeq_pq_equation"]); |
347 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; |
347 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; |
348 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; |
348 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; |
349 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; |
349 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; |
350 val (p,_,f,nxt,_,pt) = me nxt p c pt; |
350 val (p,_,f,nxt,_,pt) = me nxt p c pt; |
351 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 0, x = -1]")) => () |
351 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 0, x = -1]")) => () |
352 | _ => raise error "polyeq.sml: diff.behav. in 1*x + x^2 = 0 -> [x = 0, x = -1]"; |
352 | _ => error "polyeq.sml: diff.behav. in 1*x + x^2 = 0 -> [x = 0, x = -1]"; |
353 |
353 |
354 "----- d2_pqformula6 ------"; |
354 "----- d2_pqformula6 ------"; |
355 val fmz = ["equality (1*x + 1*x^^^2 = 0)", "solveFor x","solutions L"]; |
355 val fmz = ["equality (1*x + 1*x^^^2 = 0)", "solveFor x","solutions L"]; |
356 val (dI',pI',mI') = ("PolyEq",["pqFormula","degree_2","polynomial","univariate","equation"], |
356 val (dI',pI',mI') = ("PolyEq",["pqFormula","degree_2","polynomial","univariate","equation"], |
357 ["PolyEq","solve_d2_polyeq_pq_equation"]); |
357 ["PolyEq","solve_d2_polyeq_pq_equation"]); |
366 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; |
366 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; |
367 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; |
367 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; |
368 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; |
368 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; |
369 val (p,_,f,nxt,_,pt) = me nxt p c pt; |
369 val (p,_,f,nxt,_,pt) = me nxt p c pt; |
370 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 0, x = -1]")) => () |
370 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 0, x = -1]")) => () |
371 | _ => raise error "polyeq.sml: diff.behav. in 1*x + 1*x^2 = 0 -> [x = 0, x = -1]"; |
371 | _ => error "polyeq.sml: diff.behav. in 1*x + 1*x^2 = 0 -> [x = 0, x = -1]"; |
372 |
372 |
373 "----- d2_pqformula7 ------"; |
373 "----- d2_pqformula7 ------"; |
374 (*EP-10*) |
374 (*EP-10*) |
375 val fmz = ["equality ( x + x^^^2 = 0)", "solveFor x","solutions L"]; |
375 val fmz = ["equality ( x + x^^^2 = 0)", "solveFor x","solutions L"]; |
376 val (dI',pI',mI') = ("PolyEq",["pqFormula","degree_2","polynomial","univariate","equation"], |
376 val (dI',pI',mI') = ("PolyEq",["pqFormula","degree_2","polynomial","univariate","equation"], |
386 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; |
386 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; |
387 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; |
387 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; |
388 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; |
388 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; |
389 val (p,_,f,nxt,_,pt) = me nxt p c pt; |
389 val (p,_,f,nxt,_,pt) = me nxt p c pt; |
390 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 0, x = -1]")) => () |
390 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 0, x = -1]")) => () |
391 | _ => raise error "polyeq.sml: diff.behav. in x + x^2 = 0 -> [x = 0, x = -1]"; |
391 | _ => error "polyeq.sml: diff.behav. in x + x^2 = 0 -> [x = 0, x = -1]"; |
392 |
392 |
393 "----- d2_pqformula8 ------"; |
393 "----- d2_pqformula8 ------"; |
394 val fmz = ["equality ( x + 1*x^^^2 = 0)", "solveFor x","solutions L"]; |
394 val fmz = ["equality ( x + 1*x^^^2 = 0)", "solveFor x","solutions L"]; |
395 val (dI',pI',mI') = ("PolyEq",["pqFormula","degree_2","polynomial","univariate","equation"], |
395 val (dI',pI',mI') = ("PolyEq",["pqFormula","degree_2","polynomial","univariate","equation"], |
396 ["PolyEq","solve_d2_polyeq_pq_equation"]); |
396 ["PolyEq","solve_d2_polyeq_pq_equation"]); |
406 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; |
406 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; |
407 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; |
407 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; |
408 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; |
408 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; |
409 val (p,_,f,nxt,_,pt) = me nxt p c pt; |
409 val (p,_,f,nxt,_,pt) = me nxt p c pt; |
410 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 0, x = -1]")) => () |
410 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 0, x = -1]")) => () |
411 | _ => raise error "polyeq.sml: diff.behav. in x + 1*x^2 = 0 -> [x = 0, x = -1]"; |
411 | _ => error "polyeq.sml: diff.behav. in x + 1*x^2 = 0 -> [x = 0, x = -1]"; |
412 |
412 |
413 "----- d2_pqformula9 ------"; |
413 "----- d2_pqformula9 ------"; |
414 val fmz = ["equality (-4 + x^^^2 = 0)", "solveFor x","solutions L"]; |
414 val fmz = ["equality (-4 + x^^^2 = 0)", "solveFor x","solutions L"]; |
415 val (dI',pI',mI') = ("PolyEq",["pqFormula","degree_2","polynomial","univariate","equation"], |
415 val (dI',pI',mI') = ("PolyEq",["pqFormula","degree_2","polynomial","univariate","equation"], |
416 ["PolyEq","solve_d2_polyeq_pq_equation"]); |
416 ["PolyEq","solve_d2_polyeq_pq_equation"]); |
425 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; |
425 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; |
426 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; |
426 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; |
427 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; |
427 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; |
428 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; |
428 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; |
429 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 2, x = -2]")) => () |
429 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 2, x = -2]")) => () |
430 | _ => raise error "polyeq.sml: diff.behav. in -4 + x^2 = 0 -> [x = 2, x = -2]"; |
430 | _ => error "polyeq.sml: diff.behav. in -4 + x^2 = 0 -> [x = 2, x = -2]"; |
431 |
431 |
432 |
432 |
433 "----- d2_pqformula10_neg ------"; |
433 "----- d2_pqformula10_neg ------"; |
434 val fmz = ["equality (4 + x^^^2 = 0)", "solveFor x","solutions L"]; |
434 val fmz = ["equality (4 + x^^^2 = 0)", "solveFor x","solutions L"]; |
435 val (dI',pI',mI') = ("PolyEq",["pqFormula","degree_2","polynomial","univariate","equation"], |
435 val (dI',pI',mI') = ("PolyEq",["pqFormula","degree_2","polynomial","univariate","equation"], |
465 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; |
465 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; |
466 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; |
466 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; |
467 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; |
467 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; |
468 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; |
468 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; |
469 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 2, x = -2]")) => () |
469 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 2, x = -2]")) => () |
470 | _ => raise error "polyeq.sml: diff.behav. in -4 + 1*x^2 = 0 -> [x = 2, x = -2]"; |
470 | _ => error "polyeq.sml: diff.behav. in -4 + 1*x^2 = 0 -> [x = 2, x = -2]"; |
471 |
471 |
472 "----- d2_pqformula9_neg ------"; |
472 "----- d2_pqformula9_neg ------"; |
473 val fmz = ["equality (4 + 1*x^^^2 = 0)", "solveFor x","solutions L"]; |
473 val fmz = ["equality (4 + 1*x^^^2 = 0)", "solveFor x","solutions L"]; |
474 val (dI',pI',mI') = ("PolyEq",["pqFormula","degree_2","polynomial","univariate","equation"], |
474 val (dI',pI',mI') = ("PolyEq",["pqFormula","degree_2","polynomial","univariate","equation"], |
475 ["PolyEq","solve_d2_polyeq_pq_equation"]); |
475 ["PolyEq","solve_d2_polyeq_pq_equation"]); |
506 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; |
506 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; |
507 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; |
507 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; |
508 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; |
508 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; |
509 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; |
509 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; |
510 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 1, x = -1 / 2]")) => () |
510 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 1, x = -1 / 2]")) => () |
511 | _ => raise error "polyeq.sml: diff.behav. in -1 + (-1)*x + 2*x^2 = 0 -> [x = 1, x = -1/2]"; |
511 | _ => error "polyeq.sml: diff.behav. in -1 + (-1)*x + 2*x^2 = 0 -> [x = 1, x = -1/2]"; |
512 |
512 |
513 val fmz = ["equality ( 1 +(-1)*x + 2*x^^^2 = 0)", "solveFor x","solutions L"]; |
513 val fmz = ["equality ( 1 +(-1)*x + 2*x^^^2 = 0)", "solveFor x","solutions L"]; |
514 val (dI',pI',mI') = ("PolyEq",["abcFormula","degree_2","polynomial","univariate","equation"], |
514 val (dI',pI',mI') = ("PolyEq",["abcFormula","degree_2","polynomial","univariate","equation"], |
515 ["PolyEq","solve_d2_polyeq_abc_equation"]); |
515 ["PolyEq","solve_d2_polyeq_abc_equation"]); |
516 (*val p = e_pos'; val c = []; |
516 (*val p = e_pos'; val c = []; |
543 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; |
543 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; |
544 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; |
544 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; |
545 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; |
545 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; |
546 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; |
546 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; |
547 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 1 / 2, x = -1]")) => () |
547 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 1 / 2, x = -1]")) => () |
548 | _ => raise error "polyeq.sml: diff.behav. in -1 + x + 2*x^2 = 0 -> [x = 1/2, x = -1]"; |
548 | _ => error "polyeq.sml: diff.behav. in -1 + x + 2*x^2 = 0 -> [x = 1/2, x = -1]"; |
549 |
549 |
550 val fmz = ["equality ( 1 + x + 2*x^^^2 = 0)", "solveFor x","solutions L"]; |
550 val fmz = ["equality ( 1 + x + 2*x^^^2 = 0)", "solveFor x","solutions L"]; |
551 val (dI',pI',mI') = ("PolyEq",["abcFormula","degree_2","polynomial","univariate","equation"], |
551 val (dI',pI',mI') = ("PolyEq",["abcFormula","degree_2","polynomial","univariate","equation"], |
552 ["PolyEq","solve_d2_polyeq_abc_equation"]); |
552 ["PolyEq","solve_d2_polyeq_abc_equation"]); |
553 (*val p = e_pos'; val c = []; |
553 (*val p = e_pos'; val c = []; |
580 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; |
580 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; |
581 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; |
581 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; |
582 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; |
582 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; |
583 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; |
583 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; |
584 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 1, x = -2]")) => () |
584 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 1, x = -2]")) => () |
585 | _ => raise error "polyeq.sml: diff.behav. in -2 + 1*x + x^2 = 0 -> [x = 1, x = -2]"; |
585 | _ => error "polyeq.sml: diff.behav. in -2 + 1*x + x^2 = 0 -> [x = 1, x = -2]"; |
586 |
586 |
587 val fmz = ["equality ( 2 + 1*x + x^^^2 = 0)", "solveFor x","solutions L"]; |
587 val fmz = ["equality ( 2 + 1*x + x^^^2 = 0)", "solveFor x","solutions L"]; |
588 val (dI',pI',mI') = ("PolyEq",["abcFormula","degree_2","polynomial","univariate","equation"], |
588 val (dI',pI',mI') = ("PolyEq",["abcFormula","degree_2","polynomial","univariate","equation"], |
589 ["PolyEq","solve_d2_polyeq_abc_equation"]); |
589 ["PolyEq","solve_d2_polyeq_abc_equation"]); |
590 (*val p = e_pos'; val c = []; |
590 (*val p = e_pos'; val c = []; |
618 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; |
618 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; |
619 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; |
619 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; |
620 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; |
620 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; |
621 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; |
621 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; |
622 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 1, x = -2]")) => () |
622 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 1, x = -2]")) => () |
623 | _ => raise error "polyeq.sml: diff.behav. in -2 + x + x^2 = 0 -> [x = 1, x = -2]"; |
623 | _ => error "polyeq.sml: diff.behav. in -2 + x + x^2 = 0 -> [x = 1, x = -2]"; |
624 |
624 |
625 val fmz = ["equality ( 2 + x + x^^^2 = 0)", "solveFor x","solutions L"]; |
625 val fmz = ["equality ( 2 + x + x^^^2 = 0)", "solveFor x","solutions L"]; |
626 val (dI',pI',mI') = ("PolyEq",["abcFormula","degree_2","polynomial","univariate","equation"], |
626 val (dI',pI',mI') = ("PolyEq",["abcFormula","degree_2","polynomial","univariate","equation"], |
627 ["PolyEq","solve_d2_polyeq_abc_equation"]); |
627 ["PolyEq","solve_d2_polyeq_abc_equation"]); |
628 (*val p = e_pos'; val c = []; |
628 (*val p = e_pos'; val c = []; |
656 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; |
656 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; |
657 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; |
657 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; |
658 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; |
658 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; |
659 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; |
659 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; |
660 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 2, x = -2]")) => () |
660 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 2, x = -2]")) => () |
661 | _ => raise error "polyeq.sml: diff.behav. in -8 + 2*x^2 = 0 -> [x = 2, x = -2]"; |
661 | _ => error "polyeq.sml: diff.behav. in -8 + 2*x^2 = 0 -> [x = 2, x = -2]"; |
662 |
662 |
663 val fmz = ["equality ( 8+ 2*x^^^2 = 0)", "solveFor x","solutions L"]; |
663 val fmz = ["equality ( 8+ 2*x^^^2 = 0)", "solveFor x","solutions L"]; |
664 val (dI',pI',mI') = ("PolyEq",["abcFormula","degree_2","polynomial","univariate","equation"], |
664 val (dI',pI',mI') = ("PolyEq",["abcFormula","degree_2","polynomial","univariate","equation"], |
665 ["PolyEq","solve_d2_polyeq_abc_equation"]); |
665 ["PolyEq","solve_d2_polyeq_abc_equation"]); |
666 (*val p = e_pos'; val c = []; |
666 (*val p = e_pos'; val c = []; |
692 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; |
692 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; |
693 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; |
693 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; |
694 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; |
694 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; |
695 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; |
695 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; |
696 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 2, x = -2]")) => () |
696 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 2, x = -2]")) => () |
697 | _ => raise error "polyeq.sml: diff.behav. in -4 + x^2 = 0 -> [x = 2, x = -2]"; |
697 | _ => error "polyeq.sml: diff.behav. in -4 + x^2 = 0 -> [x = 2, x = -2]"; |
698 |
698 |
699 |
699 |
700 val fmz = ["equality ( 4+ x^^^2 = 0)", "solveFor x","solutions L"]; |
700 val fmz = ["equality ( 4+ x^^^2 = 0)", "solveFor x","solutions L"]; |
701 val (dI',pI',mI') = ("PolyEq",["abcFormula","degree_2","polynomial","univariate","equation"], ["PolyEq","solve_d2_polyeq_abc_equation"]); |
701 val (dI',pI',mI') = ("PolyEq",["abcFormula","degree_2","polynomial","univariate","equation"], ["PolyEq","solve_d2_polyeq_abc_equation"]); |
702 (*val p = e_pos'; val c = []; |
702 (*val p = e_pos'; val c = []; |
729 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; |
729 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; |
730 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; |
730 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; |
731 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; |
731 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; |
732 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; |
732 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; |
733 case f of Form' (FormKF (~1,EdUndef,_,Nundef,"[x = 0, x = -1]")) => () |
733 case f of Form' (FormKF (~1,EdUndef,_,Nundef,"[x = 0, x = -1]")) => () |
734 | _ => raise error "polyeq.sml: diff.behav. in x + x^2 = 0 -> [x = 0, x = -1]"; |
734 | _ => error "polyeq.sml: diff.behav. in x + x^2 = 0 -> [x = 0, x = -1]"; |
735 |
735 |
736 val fmz = ["equality (1*x + x^^^2 = 0)", "solveFor x","solutions L"]; |
736 val fmz = ["equality (1*x + x^^^2 = 0)", "solveFor x","solutions L"]; |
737 val (dI',pI',mI') = ("PolyEq",["abcFormula","degree_2","polynomial","univariate","equation"], |
737 val (dI',pI',mI') = ("PolyEq",["abcFormula","degree_2","polynomial","univariate","equation"], |
738 ["PolyEq","solve_d2_polyeq_abc_equation"]); |
738 ["PolyEq","solve_d2_polyeq_abc_equation"]); |
739 (*val p = e_pos'; val c = []; |
739 (*val p = e_pos'; val c = []; |
747 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; |
747 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; |
748 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; |
748 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; |
749 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; |
749 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; |
750 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; |
750 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; |
751 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 0, x = -1]")) => () |
751 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 0, x = -1]")) => () |
752 | _ => raise error "polyeq.sml: diff.behav. in x + x^2 = 0 -> [x = 0, x = -1]"; |
752 | _ => error "polyeq.sml: diff.behav. in x + x^2 = 0 -> [x = 0, x = -1]"; |
753 |
753 |
754 (*EP-16*) |
754 (*EP-16*) |
755 val fmz = ["equality (x + 2*x^^^2 = 0)", "solveFor x","solutions L"]; |
755 val fmz = ["equality (x + 2*x^^^2 = 0)", "solveFor x","solutions L"]; |
756 val (dI',pI',mI') = ("PolyEq",["abcFormula","degree_2","polynomial","univariate","equation"], |
756 val (dI',pI',mI') = ("PolyEq",["abcFormula","degree_2","polynomial","univariate","equation"], |
757 ["PolyEq","solve_d2_polyeq_abc_equation"]); |
757 ["PolyEq","solve_d2_polyeq_abc_equation"]); |
766 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; |
766 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; |
767 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; |
767 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; |
768 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; |
768 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; |
769 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; |
769 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; |
770 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 0, x = -1 / 2]")) => () |
770 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 0, x = -1 / 2]")) => () |
771 | _ => raise error "polyeq.sml: diff.behav. in x + x^2 = 0 -> [x = 0, x = -1 / 2]"; |
771 | _ => error "polyeq.sml: diff.behav. in x + x^2 = 0 -> [x = 0, x = -1 / 2]"; |
772 |
772 |
773 (*EP-//*) |
773 (*EP-//*) |
774 val fmz = ["equality (x + x^^^2 = 0)", "solveFor x","solutions L"]; |
774 val fmz = ["equality (x + x^^^2 = 0)", "solveFor x","solutions L"]; |
775 val (dI',pI',mI') = ("PolyEq",["abcFormula","degree_2","polynomial","univariate","equation"], |
775 val (dI',pI',mI') = ("PolyEq",["abcFormula","degree_2","polynomial","univariate","equation"], |
776 ["PolyEq","solve_d2_polyeq_abc_equation"]); |
776 ["PolyEq","solve_d2_polyeq_abc_equation"]); |
785 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; |
785 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; |
786 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; |
786 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; |
787 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; |
787 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; |
788 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; |
788 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; |
789 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 0, x = -1]")) => () |
789 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 0, x = -1]")) => () |
790 | _ => raise error "polyeq.sml: diff.behav. in x + x^2 = 0 -> [x = 0, x = -1]"; |
790 | _ => error "polyeq.sml: diff.behav. in x + x^2 = 0 -> [x = 0, x = -1]"; |
791 |
791 |
792 "----------- (-8 - 2*x + x^^^2 = 0), (*Schalk 2, S.67 Nr.31.b----"; |
792 "----------- (-8 - 2*x + x^^^2 = 0), (*Schalk 2, S.67 Nr.31.b----"; |
793 "----------- (-8 - 2*x + x^^^2 = 0), (*Schalk 2, S.67 Nr.31.b----"; |
793 "----------- (-8 - 2*x + x^^^2 = 0), (*Schalk 2, S.67 Nr.31.b----"; |
794 "----------- (-8 - 2*x + x^^^2 = 0), (*Schalk 2, S.67 Nr.31.b----"; |
794 "----------- (-8 - 2*x + x^^^2 = 0), (*Schalk 2, S.67 Nr.31.b----"; |
795 val fmz = ["equality (-8 - 2*x + x^^^2 = 0)", (*Schalk 2, S.67 Nr.31.b*) |
795 val fmz = ["equality (-8 - 2*x + x^^^2 = 0)", (*Schalk 2, S.67 Nr.31.b*) |
833 val (p,_,f,nxt,_,pt) = me nxt p c pt; |
833 val (p,_,f,nxt,_,pt) = me nxt p c pt; |
834 (*"[x = -2, x = 4]" nxt = Check_Postcond*) |
834 (*"[x = -2, x = 4]" nxt = Check_Postcond*) |
835 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f; |
835 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f; |
836 (* FIXXXME |
836 (* FIXXXME |
837 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = -2, x = 4]")) => () TODO |
837 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = -2, x = 4]")) => () TODO |
838 | _ => raise error "polyeq.sml: diff.behav. in [x = -2, x = 4]"; |
838 | _ => error "polyeq.sml: diff.behav. in [x = -2, x = 4]"; |
839 *) |
839 *) |
840 if f2str f = "[x = -1 * -1 + -1 * sqrt (1 ^^^ 2 - -8),\n x = -1 * -1 + -1 * (-1 * sqrt (1 ^^^ 2 - -8))]" then () |
840 if f2str f = "[x = -1 * -1 + -1 * sqrt (1 ^^^ 2 - -8),\n x = -1 * -1 + -1 * (-1 * sqrt (1 ^^^ 2 - -8))]" then () |
841 else raise error "polyeq.sml corrected?behav. in [x = -2, x = 4]"; |
841 else error "polyeq.sml corrected?behav. in [x = -2, x = 4]"; |
842 |
842 |
843 |
843 |
844 "-------------------- (3 - 10*x + 3*x^^^2 = 0), ----------------------"; |
844 "-------------------- (3 - 10*x + 3*x^^^2 = 0), ----------------------"; |
845 "-------------------- (3 - 10*x + 3*x^^^2 = 0), ----------------------"; |
845 "-------------------- (3 - 10*x + 3*x^^^2 = 0), ----------------------"; |
846 "-------------------- (3 - 10*x + 3*x^^^2 = 0), ----------------------"; |
846 "-------------------- (3 - 10*x + 3*x^^^2 = 0), ----------------------"; |
847 "---- test the erls ----"; |
847 "---- test the erls ----"; |
848 val t1 = (term_of o the o (parse thy)) "0 <= (10/3/2)^^^2 - 1"; |
848 val t1 = (term_of o the o (parse thy)) "0 <= (10/3/2)^^^2 - 1"; |
849 val SOME (t,_) = rewrite_set_ PolyEq.thy false PolyEq_erls t1; |
849 val SOME (t,_) = rewrite_set_ PolyEq.thy false PolyEq_erls t1; |
850 val t' = term2str t; |
850 val t' = term2str t; |
851 (*if t'= "True" then () |
851 (*if t'= "True" then () |
852 else raise error "polyeq.sml: diff.behav. in 'rewrite_set_.. PolyEq_erls";*) |
852 else error "polyeq.sml: diff.behav. in 'rewrite_set_.. PolyEq_erls";*) |
853 (* *) |
853 (* *) |
854 val fmz = ["equality (3 - 10*x + 3*x^^^2 = 0)", |
854 val fmz = ["equality (3 - 10*x + 3*x^^^2 = 0)", |
855 "solveFor x","solutions L"]; |
855 "solveFor x","solutions L"]; |
856 val (dI',pI',mI') = |
856 val (dI',pI',mI') = |
857 ("PolyEq",["degree_2","expanded","univariate","equation"], |
857 ("PolyEq",["degree_2","expanded","univariate","equation"], |
902 val (p,_,f,nxt,_,pt) = me nxt p c pt; |
902 val (p,_,f,nxt,_,pt) = me nxt p c pt; |
903 val (p,_,f,nxt,_,pt) = me nxt p c pt; |
903 val (p,_,f,nxt,_,pt) = me nxt p c pt; |
904 val (p,_,f,nxt,_,pt) = me nxt p c pt; |
904 val (p,_,f,nxt,_,pt) = me nxt p c pt; |
905 (* FIXXXXME n1., |
905 (* FIXXXXME n1., |
906 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 2, x = -4]")) => () TODO |
906 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 2, x = -4]")) => () TODO |
907 | _ => raise error "polyeq.sml: diff.behav. in [x = 2, x = -4]"; |
907 | _ => error "polyeq.sml: diff.behav. in [x = 2, x = -4]"; |
908 *) |
908 *) |
909 |
909 |
910 "----------- (a*b - (a+b)*x + x^^^2 = 0), (*Schalk 2,S.68Nr.44.a*)"; |
910 "----------- (a*b - (a+b)*x + x^^^2 = 0), (*Schalk 2,S.68Nr.44.a*)"; |
911 "----------- (a*b - (a+b)*x + x^^^2 = 0), (*Schalk 2,S.68Nr.44.a*)"; |
911 "----------- (a*b - (a+b)*x + x^^^2 = 0), (*Schalk 2,S.68Nr.44.a*)"; |
912 "----------- (a*b - (a+b)*x + x^^^2 = 0), (*Schalk 2,S.68Nr.44.a*)"; |
912 "----------- (a*b - (a+b)*x + x^^^2 = 0), (*Schalk 2,S.68Nr.44.a*)"; |
944 Form' |
944 Form' |
945 (FormKF |
945 (FormKF |
946 (~1,EdUndef,0,Nundef, |
946 (~1,EdUndef,0,Nundef, |
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)]")) |
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)]")) |
948 => () |
948 => () |
949 | _ => raise error "polyeq.sml: diff.behav. in a*b - (a+b)*x + x^^^2 = 0"; |
949 | _ => error "polyeq.sml: diff.behav. in a*b - (a+b)*x + x^^^2 = 0"; |
950 this will be simplified [x = a, x = b] to by Factor.ML*) |
950 this will be simplified [x = a, x = b] to by Factor.ML*) |
951 |
951 |
952 |
952 |
953 "----------- (-64 + x^^^2 = 0), (*Schalk 2, S.66 Nr.1.a~--------*)"; |
953 "----------- (-64 + x^^^2 = 0), (*Schalk 2, S.66 Nr.1.a~--------*)"; |
954 "----------- (-64 + x^^^2 = 0), (*Schalk 2, S.66 Nr.1.a~--------*)"; |
954 "----------- (-64 + x^^^2 = 0), (*Schalk 2, S.66 Nr.1.a~--------*)"; |
976 val (p,_,f,nxt,_,pt) = me nxt p c pt; |
976 val (p,_,f,nxt,_,pt) = me nxt p c pt; |
977 val (p,_,f,nxt,_,pt) = me nxt p c pt; |
977 val (p,_,f,nxt,_,pt) = me nxt p c pt; |
978 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f; |
978 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f; |
979 (*WN.2.5.03 TODO "[x = sqrt (0 - -64), x = -1 * sqrt (0 - -64)]" |
979 (*WN.2.5.03 TODO "[x = sqrt (0 - -64), x = -1 * sqrt (0 - -64)]" |
980 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 8, x = -8]")) => () |
980 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 8, x = -8]")) => () |
981 | _ => raise error "polyeq.sml: diff.behav. in [x = 8, x = -8]"; |
981 | _ => error "polyeq.sml: diff.behav. in [x = 8, x = -8]"; |
982 *) |
982 *) |
983 |
983 |
984 "----------- (-147 + 3*x^^^2 = 0), (*Schalk 2, S.66 Nr.1.b------*)"; |
984 "----------- (-147 + 3*x^^^2 = 0), (*Schalk 2, S.66 Nr.1.b------*)"; |
985 "----------- (-147 + 3*x^^^2 = 0), (*Schalk 2, S.66 Nr.1.b------*)"; |
985 "----------- (-147 + 3*x^^^2 = 0), (*Schalk 2, S.66 Nr.1.b------*)"; |
986 "----------- (-147 + 3*x^^^2 = 0), (*Schalk 2, S.66 Nr.1.b------*)"; |
986 "----------- (-147 + 3*x^^^2 = 0), (*Schalk 2, S.66 Nr.1.b------*)"; |
1002 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; |
1002 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; |
1003 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; |
1003 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; |
1004 val (p,_,f,nxt,_,pt) = me nxt p c pt; |
1004 val (p,_,f,nxt,_,pt) = me nxt p c pt; |
1005 (*WN.2.5.03 TODO "[x = sqrt (0 - -49), x = -1 * sqrt (0 - -49)]" |
1005 (*WN.2.5.03 TODO "[x = sqrt (0 - -49), x = -1 * sqrt (0 - -49)]" |
1006 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 7, x = -7]")) => () |
1006 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 7, x = -7]")) => () |
1007 | _ => raise error "polyeq.sml: diff.behav. in [x = 7, x = -7]"; |
1007 | _ => error "polyeq.sml: diff.behav. in [x = 7, x = -7]"; |
1008 *) |
1008 *) |
1009 if f2str f = "[x = sqrt (0 - -49), x = -1 * sqrt (0 - -49)]" then () |
1009 if f2str f = "[x = sqrt (0 - -49), x = -1 * sqrt (0 - -49)]" then () |
1010 else raise error "polyeq.sml CORRECTED?behav. in [x = 7, x = -7]"; |
1010 else error "polyeq.sml CORRECTED?behav. in [x = 7, x = -7]"; |
1011 |
1011 |
1012 |
1012 |
1013 "----------- (3*x - 1 - (5*x - (2 - 4*x)) = -11),(*Schalk Is86Bsp5"; |
1013 "----------- (3*x - 1 - (5*x - (2 - 4*x)) = -11),(*Schalk Is86Bsp5"; |
1014 "----------- (3*x - 1 - (5*x - (2 - 4*x)) = -11),(*Schalk Is86Bsp5"; |
1014 "----------- (3*x - 1 - (5*x - (2 - 4*x)) = -11),(*Schalk Is86Bsp5"; |
1015 "----------- (3*x - 1 - (5*x - (2 - 4*x)) = -11),(*Schalk Is86Bsp5"; |
1015 "----------- (3*x - 1 - (5*x - (2 - 4*x)) = -11),(*Schalk Is86Bsp5"; |
1050 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
1050 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
1051 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
1051 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
1052 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
1052 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
1053 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
1053 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
1054 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 2]")) => () |
1054 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 2]")) => () |
1055 | _ => raise error "polyeq.sml: diff.behav. in [x = 2]"; |
1055 | _ => error "polyeq.sml: diff.behav. in [x = 2]"; |
1056 |
1056 |
1057 |
1057 |
1058 "----------- ((x+1)*(x+2) - (3*x - 2)^^^2=.. Schalk II s.68 Bsp 37"; |
1058 "----------- ((x+1)*(x+2) - (3*x - 2)^^^2=.. Schalk II s.68 Bsp 37"; |
1059 "----------- ((x+1)*(x+2) - (3*x - 2)^^^2=.. Schalk II s.68 Bsp 37"; |
1059 "----------- ((x+1)*(x+2) - (3*x - 2)^^^2=.. Schalk II s.68 Bsp 37"; |
1060 "----------- ((x+1)*(x+2) - (3*x - 2)^^^2=.. Schalk II s.68 Bsp 37"; |
1060 "----------- ((x+1)*(x+2) - (3*x - 2)^^^2=.. Schalk II s.68 Bsp 37"; |
1095 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
1095 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
1096 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
1096 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
1097 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
1097 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
1098 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
1098 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
1099 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 2 / 15, x = 1]")) => () |
1099 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 2 / 15, x = 1]")) => () |
1100 | _ => raise error "polyeq.sml: diff.behav. in [x = 2 / 15, x = 1]"; |
1100 | _ => error "polyeq.sml: diff.behav. in [x = 2 / 15, x = 1]"; |
1101 |
1101 |
1102 |
1102 |
1103 " -4 + x^^^2 =0 "; |
1103 " -4 + x^^^2 =0 "; |
1104 " -4 + x^^^2 =0 "; |
1104 " -4 + x^^^2 =0 "; |
1105 " -4 + x^^^2 =0 "; |
1105 " -4 + x^^^2 =0 "; |
1119 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
1119 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
1120 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
1120 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
1121 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
1121 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
1122 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
1122 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
1123 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 2, x = -2]")) => () |
1123 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 2, x = -2]")) => () |
1124 | _ => raise error "polyeq.sml: diff.behav. in [x = 2, x = -2]"; |
1124 | _ => error "polyeq.sml: diff.behav. in [x = 2, x = -2]"; |
1125 |
1125 |
1126 "----------------- polyeq.sml end ------------------"; |
1126 "----------------- polyeq.sml end ------------------"; |
1127 |
1127 |
1128 (*Punkte aus dem TestBericht, die ich in rlang.sml nicht zuordnen konnte:*) |
1128 (*Punkte aus dem TestBericht, die ich in rlang.sml nicht zuordnen konnte:*) |
1129 (*WN.19.3.03 ---v-*) |
1129 (*WN.19.3.03 ---v-*) |