1 (* tests for various kinds of univariate equations.
2 Author: Richard Lang 2003
3 (c) due to copyright terms
5 These tests have not been updated with the transition Isabelle2002 --> 2011
6 # because there are many other tests on equations in other test-files
7 # some of these equations are twice, e.g. x / (x ^ 2 - 6 * x + 9) - 1 / (x ^ 2 - 3 * x) = 1 / x, x
8 # this file needs specifically much cleaning.
11 (******************************************************************
12 WN.060104 transfer marked (*E..*)examples to the exp-collection
13 # exp_IsacCore_Equ_Uni_Poly.xml from rlang.sml (*EP*) exp
14 # exp_IsacCore_Equ_Uni_Rat.xml from rlang.sml (*ER*) exp
15 # exp_IsacCore_Equ_Uni_Root.xml from rlang.sml (*EO*) exp
16 *******************************************************************)
20 (*WN.12.6.03: for TODOs search 'writeln', for simplification search MG*)
21 (* use"kbtest/rlang.sml";
24 tests over all equations implemented in his diploma thesis
25 Elementare Gleichungen der Mittelschulmathematik in der ISAC Wissensbasis,
26 Master's thesis, University of Technology, Graz, Austria, March 2003.
32 author = {Schalk, Heinz-Christian and Binder, Christian and Fertl, Walter and
33 Firneis, Friedrich and Gems, Werner and Lehner, Dieter and
34 Plihal, Andreas and Würl,Manfred},
35 title = {Mathematik für höhere technische Lehranstalten Band I},
36 publisher = {Reniets Verlag},
38 note = {Schulbuch-Nr. 942},
42 author = {Schalk, Heinz-Christian and Baumgartner, Gerhard and Binder, Christian and
43 Eder, Hans Gerhard and Fertl, Walter and Firneis, Friedrich and
44 Konstantiniuk, Peter and Plihal, Andreas and Rümmele, Goswin and
45 Steinwender, Andreas and Zangerl, Nikolaus},
46 title = {Mathematik für höhere technische Lehranstalten Band II},
47 publisher = {Reniets Verlag},
49 note = {Schulbuch-Nr. 1682},
54 Rewrite.trace_on:=false; (*true false*)
55 Refine.refine fmz ["univariate", "equation"];
57 "---- rlang.sml begin-----------------------------------";
58 (*----------------- Schalk I s.86 Bsp 5 ------------------------*)
59 "Schalk I s.86 Bsp 5 (3*x - 1 - (5*x - (2 - 4*x)) = - 11)";
60 "Schalk I s.86 Bsp 5 (3*x - 1 - (5*x - (2 - 4*x)) = - 11)";
61 "Schalk I s.86 Bsp 5 (3*x - 1 - (5*x - (2 - 4*x)) = - 11)";
63 val fmz = ["equality (3*x - 1 - (5*x - (2 - 4*x)) = - 11)",
64 "solveFor x", "solutions L"];
65 val (dI',pI',mI') = ("PolyEq",["univariate", "equation"],["no_met"]);
66 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
67 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
68 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
69 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
70 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
71 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
72 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
73 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
74 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
75 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
76 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
78 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
79 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
80 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
81 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
82 case f of Form' (Test_Out.FormKF (~1,EdUndef,0,Nundef,"[x = 2]")) => ()
83 | _ => error "rlang.sml: diff.behav. in Schalk I s.86 Bsp 5 [x = 2]";
85 (*----------------- Schalk I s.86 Bsp 19 ------------------------*)
86 "Schalk I s.86 Bsp 19 (x - 5)*(10 - x) = (3 - x)*(2 + x) + 2*(x + 20)";
87 "Schalk I s.86 Bsp 19 (x - 5)*(10 - x) = (3 - x)*(2 + x) + 2*(x + 20)";
88 "Schalk I s.86 Bsp 19 (x - 5)*(10 - x) = (3 - x)*(2 + x) + 2*(x + 20)";
90 val fmz = ["equality ((x - 5)*(10 - x) = (3 - x)*(2 + x) + 2*(x + 20))",
91 "solveFor x", "solutions L"];
92 val (dI',pI',mI') = ("PolyEq",["univariate", "equation"],["no_met"]);
93 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
94 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
95 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
96 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
97 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
98 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
99 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
100 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
101 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
102 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
103 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
104 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
105 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
106 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
107 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
108 case f of Form' (Test_Out.FormKF (~1,EdUndef,0,Nundef,"[x = 8]")) => ()
109 | _ => error "rlang.sml: diff.behav. in Schalk I s.86 Bsp 19 [x = 8]";
111 (*----------------- Schalk I s.86 Bsp 23 ------------------------*)
112 "Schalk I s.86 Bsp 19 ((2*x+5) \<up> 2+(3*x+4) \<up> 2=(13*x+2)*(x+1)+2*(15+14*x))";
113 "Schalk I s.86 Bsp 19 ((2*x+5) \<up> 2+(3*x+4) \<up> 2=(13*x+2)*(x+1)+2*(15+14*x))";
114 "Schalk I s.86 Bsp 19 ((2*x+5) \<up> 2+(3*x+4) \<up> 2=(13*x+2)*(x+1)+2*(15+14*x))";
116 val fmz = ["equality ((2*x+5) \<up> 2+(3*x+4) \<up> 2=(13*x+2)*(x+1)+2*(15+14*x))",
117 "solveFor x", "solutions L"];
118 val (dI',pI',mI') = ("PolyEq",["univariate", "equation"],["no_met"]);
119 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
120 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
121 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
122 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
123 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
124 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
125 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
126 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
127 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
128 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
129 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
130 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
131 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
132 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
133 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
134 case f of Form' (Test_Out.FormKF (~1,EdUndef,0,Nundef,"[x = -9]")) => ()
135 | _ => error "rlang.sml: diff.behav. in Schalk I s.86 Bsp 23 [x = -9]";
137 (*----------------- Schalk I s.86 Bsp 25 ------------------------*)
138 "Schalk I s.86 Bsp 25 ((2*x+1) \<up> 3+(x+1) \<up> 3=(2*x+1) \<up> 2*2*x+(x+2) \<up> 3+x \<up> 2)";
139 "Schalk I s.86 Bsp 25 ((2*x+1) \<up> 3+(x+1) \<up> 3=(2*x+1) \<up> 2*2*x+(x+2) \<up> 3+x \<up> 2)";
140 "Schalk I s.86 Bsp 25 ((2*x+1) \<up> 3+(x+1) \<up> 3=(2*x+1) \<up> 2*2*x+(x+2) \<up> 3+x \<up> 2)";
142 val fmz = ["equality ((2*x+1) \<up> 3+(x+1) \<up> 3=(2*x+1) \<up> 2*2*x+(x+2) \<up> 3+x \<up> 2)",
143 "solveFor x", "solutions L"];
144 val (dI',pI',mI') = ("PolyEq",["univariate", "equation"],["no_met"]);
145 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
146 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
147 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
148 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
149 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
150 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
151 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
152 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
153 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
154 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
155 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
156 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
157 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
158 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
159 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
160 case f of Form' (Test_Out.FormKF (~1,EdUndef,0,Nundef,"[x = -6 / 5]")) => ()
161 | _ => error "rlang.sml: diff.behav. in Schalk I s.86 Bsp 25 [x = -6 / 5]";
163 (*----------------- Schalk I s.86 Bsp 28b ------------------------*)
164 "Schalk I s.86 Bsp 28b ((3*x+5)/18 - x/2 = -((3*x - 2)/9))";
165 "Schalk I s.86 Bsp 28b ((3*x+5)/18 - x/2 = -((3*x - 2)/9))";
166 "Schalk I s.86 Bsp 28b ((3*x+5)/18 - x/2 = -((3*x - 2)/9))";
168 val fmz = ["equality ((3*x+5)/18 - x/2 = -((3*x - 2)/9))",
169 "solveFor x", "solutions L"];
170 val (dI',pI',mI') = ("PolyEq",["univariate", "equation"],["no_met"]);
171 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
172 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
173 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
174 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
175 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
176 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
177 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
178 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
179 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
180 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
181 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
182 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
183 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
184 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; f2str f;
185 case f of Form' (Test_Out.FormKF (~1,EdUndef,0,Nundef,"[]")) => ()
186 | _ => error "rlang.sml: diff.behav. in Schalk I s.86 Bsp 28b []";
189 val bdv= (Thm.term_of o the o (TermC.parse thy)) "bdv";
190 val v = (Thm.term_of o the o (TermC.parse thy)) "x";
191 val t = (Thm.term_of o the o (TermC.parse thy)) "3 * x / 5";
192 val SOME (t',_) = rewrite_set_inst_ PolyEq.thy true
193 [ (bdv, v) ] make_ratpoly_in t;
194 if UnparseC.term t' = "3 / 5 * x" then () else error "rlang.sml: 1";
196 val t = TermC.parse_test @{context} "(3*x+5)/18 - x/2 - -(3*x - 2)/9 = 0";
197 val subst = [(TermC.parse_test @{context} "bdv", TermC.parse_test @{context} "x")];
198 val SOME (t',_) = rewrite_set_inst_ thy false subst make_ratpoly_in t;
199 if UnparseC.term t' = "1 / 18 = 0" then () else error "rlang.sml: 2";
202 (*----------------- Schalk I s.87 Bsp 36b ------------------------*)
203 "Schalk I s.87 Bsp 36b ((17*x - 51)/9 - (-(13*x - 3)/6) + 11 -(9*x- 7)/4 = 0)";
204 "Schalk I s.87 Bsp 36b ((17*x - 51)/9 - (-(13*x - 3)/6) + 11 -(9*x- 7)/4 = 0)";
205 "Schalk I s.87 Bsp 36b ((17*x - 51)/9 - (-(13*x - 3)/6) + 11 -(9*x- 7)/4 = 0)";
207 val fmz = ["equality ((17*x - 51)/9 - (-(13*x - 3)/6) + 11 - (9*x - 7)/4 = 0)",
208 "solveFor x", "solutions L"];
209 val (dI',pI',mI') = ("PolyEq",["univariate", "equation"],["no_met"]);
210 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
211 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
212 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
213 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
214 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
215 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
216 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
217 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
218 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
219 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
220 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
221 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
222 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
223 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
224 case f of Form' (Test_Out.FormKF (~1,EdUndef,0,Nundef,"[x = - 237 / 65]")) => ()
225 | _ => error "rlang.sml: diff.behav. in Schalk I s.86 Bsp 36b [x = - 237 / 65]";
229 val t = TermC.parse_test @{context} "(17*x - 51)/9 - (-(13*x - 3)/6) + 11 - (9*x - 7)/4 = 0";
230 val subst = [(TermC.parse_test @{context} "bdv", TermC.parse_test @{context} "x")];
231 val SOME (t',_) = rewrite_set_inst_ thy false subst make_ratpoly_in t;
233 if UnparseC.term t' = "79 / 12 + 65 / 36 * x = 0" then ()
234 else error "rlang.sml: 3";
238 (*----------------- Schalk I s.87 Bsp 38b ------------------------*)
239 "Schalk I s.87 Bsp 38b (-(2/x) + 3/(2*x) - 4/(3*x) + 5/(4*x) + 6/(5*x) =65/8)";
240 "Schalk I s.87 Bsp 38b (-(2/x) + 3/(2*x) - 4/(3*x) + 5/(4*x) + 6/(5*x) =65/8)";
241 "Schalk I s.87 Bsp 38b (-(2/x) + 3/(2*x) - 4/(3*x) + 5/(4*x) + 6/(5*x) =65/8)";
243 val fmz = ["equality (- 2/x + 3/(2*x) - 4/(3*x) + 5/(4*x) + 6/(5*x) = 65/8)",
244 "solveFor x", "solutions L"];
245 val (dI',pI',mI') = ("RatEq",["univariate", "equation"],["no_met"]);
246 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
247 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
248 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
249 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
250 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
251 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
252 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
253 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
254 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
255 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
256 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
257 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
258 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
259 if f = Form' (Test_Out.FormKF (~1, EdUndef, 0, Nundef, "296 + -3900 * x = 0")) then ()
260 else error "rlang.sml: diff.behav. in Schalk I s.87 Bsp 38b";
261 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
262 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
263 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
264 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
265 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
266 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
267 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
268 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
269 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
270 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
271 case f of Form' (Test_Out.FormKF (~1,EdUndef,0,Nundef,"[x = 74 / 975]")) => ()
272 | _ => error "rlang.sml: diff.behav. in Schalk I s.86 Bsp 38b [x = 74 / 975]";
274 (*----------------- Schalk I s.87 Bsp 40b ------------------------*)
275 "Schalk I s.87 Bsp 40b ((x+3)/(2*x - 4)=3)";
276 "Schalk I s.87 Bsp 40b ((x+3)/(2*x - 4)=3)";
277 "Schalk I s.87 Bsp 40b ((x+3)/(2*x - 4)=3)";
279 val fmz = ["equality ((x+3)/(2*x - 4)=3)",
280 "solveFor x", "solutions L"];
281 val (dI',pI',mI') = ("RatEq",["univariate", "equation"],["no_met"]);
282 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
283 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
284 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
285 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
286 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
287 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
288 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
289 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
290 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
291 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
292 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
293 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
294 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; f2str f;
295 (*val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
296 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;*)
297 if f = Form' (Test_Out.FormKF (~1, EdUndef, 0, Nundef, "15 + -5 * x = 0")) then ()
298 else error "rlang.sml: diff.behav. in Schalk I s.87 Bsp 40b";
299 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
300 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
301 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
302 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
303 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
304 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
305 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
306 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
307 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
308 case f of Form' (Test_Out.FormKF (~1,EdUndef,0,Nundef,"[x = 3]")) => ()
309 | _ => error "rlang.sml: diff.behav. in Schalk I s.87 Bsp 40b [x = 3]";
312 (*----------------- Schalk I s.87 Bsp 44a ------------------------*)
313 "Schalk I s.87 Bsp 44a ((1/2+(5*x)/2) \<up> 2 -((13*x)/2- 5/2) \<up> 2 -(6*x) \<up> 2+29)";
314 "Schalk I s.87 Bsp 44a ((1/2+(5*x)/2) \<up> 2 -((13*x)/2- 5/2) \<up> 2 -(6*x) \<up> 2+29)";
315 "Schalk I s.87 Bsp 44a ((1/2+(5*x)/2) \<up> 2 -((13*x)/2- 5/2) \<up> 2 -(6*x) \<up> 2+29)";
317 val fmz = ["equality ((1/2 + (5*x)/2) \<up> 2 - ((13*x)/2 - 5/2) \<up> 2 = - 1*(6*x) \<up> 2 + 29)",
318 "solveFor x", "solutions L"];
319 val (dI',pI',mI') = ("PolyEq",["univariate", "equation"],["no_met"]);
320 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
321 Rewrite.trace_on:=true; (*true false*)
323 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
324 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
325 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
326 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
327 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
328 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
329 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
330 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
331 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
332 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
333 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
334 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
335 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
336 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
337 case f of Form' (Test_Out.FormKF (~1,EdUndef,0,Nundef,"[x = 1]")) => ()
338 | _ => error "rlang.sml: diff.behav. in Schalk I s.87 Bsp 44a [x = 1]";
341 val t = TermC.parse_test @{context} "(1/2 + (5*x)/2) \<up> 2 - ((13*x)/2 - 5/2) \<up> 2 - (6*x) \<up> 2 + 29";
342 val subst = [(TermC.parse_test @{context} "bdv", TermC.parse_test @{context} "x")];
343 val SOME (t',_) = rewrite_set_inst_ thy false subst make_ratpoly_in t;
344 if UnparseC.term t' = "23 + 35 * x + -72 * x \<up> 2" then ()
345 else error "rlang.sml: 4";
347 val t = TermC.parse_test @{context} "(1/2 + (5*x)/2) \<up> 2 - ((13*x)/2 - 5/2) \<up> 2 + (6*x) \<up> 2 - 29";
348 val subst = [(TermC.parse_test @{context} "bdv", TermC.parse_test @{context} "x")];
349 val SOME (t',_) = rewrite_set_inst_ thy false subst make_ratpoly_in t;
350 if UnparseC.term t' = "-35 + 35 * x" then ()
351 else error "rlang.sml: 4.1";
354 (*----------------- Schalk I s.88 Bsp 64c ------------------------*)
355 "Schalk I s.88 Bsp 64c (((x - 1)/(x+1)+1)/((x - 1)/(x+1) - (x+1)/(x - 1))=2)";
356 "Schalk I s.88 Bsp 64c (((x - 1)/(x+1)+1)/((x - 1)/(x+1) - (x+1)/(x - 1))=2)";
357 "Schalk I s.88 Bsp 64c (((x - 1)/(x+1)+1)/((x - 1)/(x+1) - (x+1)/(x - 1))=2)";
359 val fmz = ["equality (((x - 1)/(x+1)+1)/((x - 1)/(x+1) - (x+1)/(x - 1))=2)",
360 "solveFor x", "solutions L"];
361 val (dI',pI',mI') = ("RatEq",["univariate", "equation"],["no_met"]);
363 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
364 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
365 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
366 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
367 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
368 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
369 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
370 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
371 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
372 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
373 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
374 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
375 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; f2str f;
376 if f = Form' (Test_Out.FormKF (~1, EdUndef, 0, Nundef, "-3 + - 1 * x = 0")) then ()
377 else error "rlangsml: diff.behav. in Schalk I s.88 Bsp 64c";
378 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
379 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
380 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
381 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
382 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
383 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
384 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
385 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
386 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
387 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
388 case f of Form' (Test_Out.FormKF (_,_,0,_,"[x = -3]")) => ()
389 | _ => error "rlang.sml: diff.behav. in Schalk I s.88 Bsp 64c [x = -3]";
391 (*----------------- Schalk I s.88 Bsp 79a (2) ------------------------*)
392 "Schalk I s.88 Bsp 79a (2) (m1*v1+m2*v2=0)";
393 "Schalk I s.88 Bsp 79a (2) (m1*v1+m2*v2=0)";
394 "Schalk I s.88 Bsp 79a (2) (m1*v1+m2*v2=0)";
396 val fmz = ["equality (m1*v1+m2*v2=0)",
397 "solveFor m1", "solutions L"];
398 val (dI',pI',mI') = ("PolyEq",["univariate", "equation"],["no_met"]);
400 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
401 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
402 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
403 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
404 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
405 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
406 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
407 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
408 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
409 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
410 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
411 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
412 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
413 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
414 case f of Form' (Test_Out.FormKF (~1,EdUndef,0,Nundef,"[m1 = - 1 * m2 * v2 / v1]")) => ()
415 | _ => error "rlang.sml: diff.behav. in Schalk I s.88 Bsp 79a (2) [m1 = - 1 * m2 * v2 / v1]";
417 (*----------------- Schalk I s.89 Bsp 90a(1) ------------------------*)
418 "Schalk I s.89 Bsp 90a (1) (f=((w+u)/(w+v))*v0)";
419 "Schalk I s.89 Bsp 90a (1) (f=((w+u)/(w+v))*v0)";
420 "Schalk I s.89 Bsp 90a (1) (f=((w+u)/(w+v))*v0)";
422 val fmz = ["equality (f=((w+u)/(w+v))*v0)",
423 "solveFor v", "solutions L"];
424 val (dI',pI',mI') = ("RatEq",["univariate", "equation"],["no_met"]);
426 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
427 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
428 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
429 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
430 (*val nxt = Specify_Problem ["rational", "univariate", "equation"]) *)
431 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
432 (*val nxt = Specify_Method ["RatEq", "solve_rat_equation"]) *)
433 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
434 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
435 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
436 (*nxt = Subproblem ("RatEq",["univariate", "equation"])) *)
437 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
438 (*val nxt =Model_Problem ["normalise", "polynomial", "univariate", "equation"])*)
439 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
440 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
441 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
442 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
443 (*val nxt = ("Apply_Method",Apply_Method ["PolyEq", "normalise_poly"])*)
444 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
445 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
446 (*val nxt =Subproblem ("PolyEq",["polynomial", "univariate", "equation"]))*)
453 "f * w + - 1 * u * v0 + - 1 * v0 * w + f * v = 0")) then ()
454 else error "rlang.sml: diff.behav. in Schalk I s.89 Bsp 90a";
455 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
456 (*val nxt = Model_Problem ["degree_1", "polynomial", "univariate", "equation"])*)
457 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
458 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
459 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
460 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
461 (*val nxt = ("Apply_Method",Apply_Method ["PolyEq", "solve_d1_poly_equation"])*)
462 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
463 (*val f = "v = - 1 * (f * w + - 1 * u * v0 + - 1 * v0 * w) / f")) : mout
464 val nxt = ("Or_to_List",Or_to_List) : string * tac *)
465 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
466 (*val f = "[v = - 1 * (f * w + - 1 * u * v0 + - 1 * v0 * w) / f]")) : mout
467 val nxt = ("Check_elementwise",Check_elementwise "Assumptions") *)
468 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
469 (*val f = "[v = - 1 * (f * w + - 1 * u * v0 + - 1 * v0 * w) / f]")) : mout
470 val nxt = Check_Postcond ["degree_1", "polynomial", "univariate", "equation"])*)
471 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
472 (*val f = "[v = - 1 * (f * w + - 1 * u * v0 + - 1 * v0 * w) / f]")) : mout
473 val nxt = Check_Postcond ["normalise", "polynomial", "univariate", "equation"])*)
474 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
475 (*val f = "[v = - 1 * (f * w + - 1 * u * v0 + - 1 * v0 * w) / f]")) : mout
476 val nxt = ("Check_elementwise",Check_elementwise "Assumptions")*)
478 Ctree.get_assumptions pt p;
479 (*it = ["v + w ~= 0"] ... goes to the solution as an assumption*)
481 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
482 (*val f = Form' (Test_Out.FormKF (~1,EdUndef,1,Nundef,"[]")) : mout
483 val nxt = Check_Postcond ["rational", "univariate", "equation"]) *)
484 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
485 case f of Form' (Test_Out.FormKF (~1,EdUndef,0,Nundef,
486 "[v = (u * v0 + v0 * w + - 1 * f * w) / f]")) => ()
487 | _ => error "rlang.sml: diff.behav. in Schalk I s.89 Bsp 90a (1) [v=...]";
488 if Ctree.get_assumptions pt p =
489 [TermC.parse_test @{context}"(u * v0 + v0 * w + - 1 * f * w) / f + w ~= 0"] then ()
490 else error "rlang.sml: diff.behav. in I s.89 Bsp 90a (1) [v=...] asm";
493 (*----------------- Schalk I s.89 Bsp 90a(2) ------------------------*)
494 "Schalk I s.89 Bsp 90a (2) (f=((w+u)/(w+v))*v0)";
495 "Schalk I s.89 Bsp 90a (2) (f=((w+u)/(w+v))*v0)";
496 "Schalk I s.89 Bsp 90a (2) (f=((w+u)/(w+v))*v0)";
498 val fmz = ["equality (f=((w+u)/(w+v))*v0)",
499 "solveFor w", "solutions L"];
500 val (dI',pI',mI') = ("RatEq",["univariate", "equation"],["no_met"]);
501 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
502 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
503 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
504 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
505 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
506 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
507 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
508 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
509 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
510 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
511 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
512 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
519 "f * v + - 1 * u * v0 + (f + - 1 * v0) * w = 0")) then ()
520 else error "rlang.sml: diff.behav. in Schalk I s.89 Bsp 90a (2)";
521 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
522 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
523 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
524 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
525 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
526 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
527 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
528 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
529 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
530 case f of Form' (Test_Out.FormKF (~1,EdUndef,0,Nundef,"[w = (u * v0 + - 1 * f * v) / (f + - 1 * v0)]")) => ()
531 | _ => error "rlang.sml: diff.behav. in Schalk I Bsp 90a(2)";
532 if Ctree.get_assumptions pt p =
533 [TermC.parse_test @{context}"v + (u * v0 + - 1 * f * v) / (f + - 1 * v0) ~= 0",
534 TermC.parse_test @{context}"f + - 1 * v0 ~= 0"]
535 then writeln "asm should be simplified ???"
536 else error "rlang.sml: diff.behav. in Schalk I Bsp 90a(2) asm";
538 (*----------------- Schalk I s.89 Bsp 98a(1) ------------------------*)
539 "Schalk I s.89 Bsp 98a (1) (1/R=1/R1+1/R2)";
540 "Schalk I s.89 Bsp 98a (1) (1/R=1/R1+1/R2)";
541 "Schalk I s.89 Bsp 98a (1) (1/R=1/R1+1/R2)";
543 val fmz = ["equality (1/R=1/R1+1/R2)",
544 "solveFor R1", "solutions L"];
545 val (dI',pI',mI') = ("RatEq",["univariate", "equation"],["no_met"]);
546 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
547 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
548 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
549 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
550 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
551 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
552 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
553 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
554 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
555 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
556 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
557 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
558 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
561 (~1, EdUndef, 0, Nundef, "- 1 * R * R2 + (R2 + - 1 * R) * R1 = 0"))then()
562 else error "rlang.sml: diff.behav. in Schalk I s.89 Bsp 98a (1)";
563 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
564 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
565 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
566 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
567 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
568 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
569 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
570 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
571 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
572 case f of Form' (Test_Out.FormKF (~1,EdUndef,0,Nundef,"[R1 = R * R2 / (R2 + - 1 * R)]")) => ()
573 | _ => error "rlang.sml: diff.behav. in 98a(1) [R1 = ...]";
574 if Ctree.get_assumptions pt p = [TermC.parse_test @{context}"R * R2 * R2 ~= (R2 + - 1 * R) * 0",
575 TermC.parse_test @{context}"R2 + - 1 * R ~= 0",
576 TermC.parse_test @{context}"R2 + - 1 * R ~= 0"]
577 then writeln "asm should be simplified"
578 else error "rlang.sml: diff.behav. in 98a(1) asm";
580 (*----------------- Schalk I s.89 Bsp 104a(1) ------------------------*)
581 "Schalk I s.89 Bsp 104a (1) (y \<up> 2=2*p*x)";
582 "Schalk I s.89 Bsp 104a (1) (y \<up> 2=2*p*x)";
583 "Schalk I s.89 Bsp 104a (1) (y \<up> 2=2*p*x)";
584 (*ER- 13 + EO- 11 ?!?*)
585 val fmz = ["equality (y \<up> 2=2*p*x)",
586 "solveFor p", "solutions L"];
587 val (dI',pI',mI') = ("PolyEq",["univariate", "equation"],["no_met"]);
588 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
589 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
590 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
591 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
592 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
593 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
594 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
595 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
596 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
597 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
598 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
599 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
600 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
601 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
602 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
603 case f of Form' (Test_Out.FormKF (_,_,0,_,"[p = y \<up> 2 / (2 * x)]")) => ()
604 | _ => error "rlang.sml: diff.behav. in Schalk I s.89 Bsp 104a (1) [p = y^2/(2*x)]";
605 if Ctree.get_assumptions pt p = [TermC.parse_test @{context}"- 2 * x ~= 0"]
606 then writeln"should be x ~= 0\nshould be x ~= 0\nshould be x ~= 0\n"
607 else error "rlang.sml: diff.behav. in I s.89 Bsp 104a(1) asm";
610 (*----------------- Schalk I s.89 Bsp 104a(2) ------------------------*)
611 "Schalk I s.89 Bsp 104a (2) (y \<up> 2=2*p*x)";
612 "Schalk I s.89 Bsp 104a (2) (y \<up> 2=2*p*x)";
613 "Schalk I s.89 Bsp 104a (2) (y \<up> 2=2*p*x)";
615 val fmz = ["equality (y \<up> 2=2*p*x)",
616 "solveFor y", "solutions L"];
617 val (dI',pI',mI') = ("PolyEq",["univariate", "equation"],["no_met"]);
618 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
619 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
620 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
621 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
622 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
623 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
624 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
625 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
626 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
627 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
628 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
629 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
630 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
631 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
632 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
633 case f of Form' (Test_Out.FormKF (_,_,0,_,"[y = sqrt (2 * p * x), y = - 1 * sqrt (2 * p * x)]")) => ()
634 | _ => error "rlang.sml: diff.behav. Schalk I s.89 Bsp 104a(2) [x = ]";
635 if Ctree.get_assumptions pt p = [TermC.parse_test @{context}"0 <= - 1 * (- 2 * p * x)",
636 TermC.parse_test @{context}"0 <= - 1 * (- 2 * p * x)"]
637 then writeln "asm should be simplified\nshould be simplified"
638 else error "rlang.sml: diff.behav. in I s.89 Bsp 104a(2) asm";
641 (*----------------- Schalk I s.90 Bsp 118a (1) ------------------------*)
642 "Schalk I s.90 Bsp 118a (1) (b \<up> 2*x \<up> 2 + a \<up> 2*y \<up> 2 = a \<up> 2*b \<up> 2)";
643 "Schalk I s.90 Bsp 118a (1) (b \<up> 2*x \<up> 2 + a \<up> 2*y \<up> 2 = a \<up> 2*b \<up> 2)";
644 "Schalk I s.90 Bsp 118a (1) (b \<up> 2*x \<up> 2 + a \<up> 2*y \<up> 2 = a \<up> 2*b \<up> 2)";
646 val fmz = ["equality (b \<up> 2*x \<up> 2 + a \<up> 2*y \<up> 2 = a \<up> 2*b \<up> 2)",
647 "solveFor x", "solutions L"];
648 val (dI',pI',mI') = ("PolyEq",["univariate", "equation"],["no_met"]);
649 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
650 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
651 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
652 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
654 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
655 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;f2str f;
656 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;f2str f;
657 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;f2str f;
659 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
660 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
661 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
662 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
663 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
664 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
665 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
666 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
667 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;f2str f;
668 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;f2str f;Ctree.get_assumptions pt p;
669 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;f2str f;Ctree.get_assumptions pt p;
670 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;f2str f;Ctree.get_assumptions pt p;
671 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;f2str f;Ctree.get_assumptions pt p;
672 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;f2str f;UnparseC.terms (*WN1104changed*) (Ctree.get_assumptions pt p);
673 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;f2str f;UnparseC.terms (*WN1104changed*) (Ctree.get_assumptions pt p);
675 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;f2str f;Ctree.get_assumptions pt p;
676 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;f2str f;Ctree.get_assumptions pt p;
677 case f of Form' (Test_Out.FormKF (~1,EdUndef,0,Nundef,"[x = sqrt ((a \<up> 2 * b \<up> 2 + - 1 * a \<up> 2 * y \<up> 2) / b \<up> 2),\n x = - 1 * sqrt ((a \<up> 2 * b \<up> 2 + - 1 * a \<up> 2 * y \<up> 2) / b \<up> 2)]")) => writeln"should be simplified MG"
678 | _ => error "rlang.sml: diff.behav. in Schalk I s.89 Bsp 118a(2) [x = ]";
679 val asms = Ctree.get_assumptions pt p;
681 [TermC.parse_test @{context}"0 * b \<up> 2 <= - 1 * (a \<up> 2 * y \<up> 2 + - 1 * a \<up> 2 * b \<up> 2)",
682 TermC.parse_test @{context}"b \<up> 2 ~= 0",
683 TermC.parse_test @{context}"0 * b \<up> 2 <= - 1 * (a \<up> 2 * y \<up> 2 + - 1 * a \<up> 2 * b \<up> 2)",
684 TermC.parse_test @{context}"b \<up> 2 ~= 0"] then writeln"should be simplified MG"
685 else error "rlang.sml: diff.behav. in Schalk I s.89 Bsp 118a(2) asms";
687 (*----------------- Schalk I s.102 Bsp 268(1) ------------------------*)
688 "Schalk I s.102 Bsp 268(1) (A = (1/2)*(x1*(y2-y3)+x2*(y3 - y1)+x3*(y1 - y2)))";
689 "Schalk I s.102 Bsp 268(1) (A = (1/2)*(x1*(y2-y3)+x2*(y3 - y1)+x3*(y1 - y2)))";
690 "Schalk I s.102 Bsp 268(1) (A = (1/2)*(x1*(y2-y3)+x2*(y3 - y1)+x3*(y1 - y2)))";
692 val fmz = ["equality (A = (1/2)*(x1*(y2 - y3)+x2*(y3 - y1)+x3*(y1 - y2)))",
693 "solveFor x2", "solutions L"];
694 val (dI',pI',mI') = ("PolyEq",["univariate", "equation"],["no_met"]);
695 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
696 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
697 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
698 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
699 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
700 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
701 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
702 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
703 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
704 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
705 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
706 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
707 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
708 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
709 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
710 case f of Form' (Test_Out.FormKF (~1,EdUndef,0,Nundef,"[x2 =\n (- 2 * A + x1 * y2 + x3 * y1 + - 1 * x1 * y3 + - 1 * x3 * y2) /\n (y1 + - 1 * y3)]")) => ()
711 | _ => error "rlang.sml: diff.behav. Schalk I s.102 Bsp 268(1) [x2=...]";
712 if Ctree.get_assumptions pt p = [TermC.parse_test @{context}"y1 / 2 + - 1 * y3 / 2 ~= 0"] then ()
713 else error "rlang.sml: diff.behav. in I s.102 Bsp 268(1) asm";
715 (*-------------------- Schalk II ----------------------------*)
716 (*-------------------- Schalk II ----------------------------*)
717 (*-------------------- Schalk II ----------------------------*)
718 (*-------------------- Schalk II ----------------------------*)
719 (*-------------------- Schalk II ----------------------------*)
722 (*----------------- Schalk II s.56 Bsp 67b ------------------------*)
723 "Schalk II s.56 Bsp 67b (4*sqrt(4*x+1)=3*sqrt(7*x+2))";
724 "Schalk II s.56 Bsp 67b (4*sqrt(4*x+1)=3*sqrt(7*x+2))";
725 "Schalk II s.56 Bsp 67b (4*sqrt(4*x+1)=3*sqrt(7*x+2))";
727 val fmz = ["equality (4*sqrt(4*x+1)=3*sqrt(7*x+2))",
728 "solveFor x", "solutions L"];
729 val (dI',pI',mI') = ("RootEq",["univariate", "equation"],["no_met"]);
730 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
731 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
732 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
733 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
734 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
735 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
736 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
737 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
738 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
739 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
740 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
741 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
742 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; f2str f;
743 if f = Form' (Test_Out.FormKF (~1, EdUndef, 0, Nundef, "- 2 + x = 0")) then ()
744 else error "rlang.sml: diff.behav. in Schalk II s.56 Bsp 67b";
745 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
746 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
747 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
748 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
749 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
750 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
751 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
752 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
753 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
754 case f of Form' (Test_Out.FormKF (~1,EdUndef,0,Nundef,"[x = 2]")) => ()
755 | _ => error "rlang.sml: diff.behav. in Schalk II s.56 Bsp 67b [x=2]";
757 (*----------------- Schalk II s.56 Bsp 68a ------------------------*)
758 "Schalk II s.56 Bsp 68a (5*sqrt(x) - 1 = 7*sqrt(x) - 5)";
759 "Schalk II s.56 Bsp 68a (5*sqrt(x) - 1 = 7*sqrt(x) - 5)";
760 "Schalk II s.56 Bsp 68a (5*sqrt(x) - 1 = 7*sqrt(x) - 5)";
761 val fmz = ["equality (5*sqrt(x) - 1 = 7*sqrt(x) - 5)",
762 "solveFor x", "solutions L"];
763 val (dI',pI',mI') = ("RootEq",["univariate", "equation"],["no_met"]);
764 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
765 (* val nxt = ("Model_Problem",Model_Problem ["normalise", "rootX", "univariate", "equation"])*)
766 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
767 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
768 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
769 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
770 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
771 (* val nxt = ("Model_Problem",Model_Problem ["sq", "rootX", "univariate", "equation"]) *)
772 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
773 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
774 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
775 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
776 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
777 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
778 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
779 (* val nxt = ("Model_Problem",Model_Problem ["sq", "rootX", "univariate", "equation"]) *)
780 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
781 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
782 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
783 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
784 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
785 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
786 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
787 Ctree.get_assumptions pt p;
788 (* val nxt = ("Model_Problem", Model_Problem ["normalise", "polynomial", "univariate", "equation"])*)
789 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
790 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
791 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
792 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
793 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
796 (~1, EdUndef, 0, Nundef, "256 + - 2368 * x + 576 * x \<up> 2 = 0"))then()
797 else error "rlang.sml: diff.behav. in Schalk II s.56 Bsp 68a";
798 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
799 Ctree.get_assumptions pt p;
800 (* val nxt = ("Model_Problem", Model_Problem
801 ["abcFormula", "degree_2", "polynomial", "univariate", "equation"])*)
802 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
803 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
804 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
805 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
806 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
807 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
808 Ctree.get_assumptions pt p;
809 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
810 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
811 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
812 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
813 if f = Form' (Test_Out.FormKF (~1,EdUndef,0,Nundef,"[x = 4, x = 1 / 9]"))
814 then writeln "only [x = 4] !\nonly [x = 4] !\nonly [x = 4] !\n"
815 else error "rlang.sml: diff.behav. in II 68a";
816 val asms = Ctree.get_assumptions pt p;
817 if UnparseC.terms (*WN1104changed*) asms =
818 "[0 <= (25 * (1 / 9) + - 1 * (16 + 49 * (1 / 9))) * -56,\
821 \0 <= (-5 + 7 * sqrt (1 / 9) + 1) * 5,\
823 \0 <= (25 * (1 / 9) + - 1 * (16 + 49 * (1 / 9))) * -56,\
825 (*WN050916 before correction 'rewrite__set_ called with 'Rule_Set.Empty' for ..'
826 thus: maybe the rls for the asms is Rule_Set.Empty ??:
827 [(TermC.parse_test @{context}"0 <= (25 * (1 / 9) + - 1 * (16 + 49 * (1 / 9))) * -56", []),
828 (TermC.parse_test @{context}"9 ~= 0", []),
829 (TermC.parse_test @{context}"0 <= (-5 + 7 * sqrt (1 / 9) + 1) * 5", []),
830 (TermC.parse_test @{context}"9 ~= 0", []),
831 (TermC.parse_test @{context}"0 <= (25 * (1 / 9) + - 1 * (16 + 49 * (1 / 9))) * -56", [])]*)
832 then "should get True * False!!!"
833 else error "rlang.sml: diff.behav. in II 68a asms";
835 (*----------------- Schalk II s.56 Bsp 73b ------------------------*)
836 "Schalk II s.56 Bsp 73b (sqrt(x+1)+sqrt(4*x+4)=sqrt(9*x+9))";
837 "Schalk II s.56 Bsp 73b (sqrt(x+1)+sqrt(4*x+4)=sqrt(9*x+9))";
838 "Schalk II s.56 Bsp 73b (sqrt(x+1)+sqrt(4*x+4)=sqrt(9*x+9))";
840 val fmz = ["equality (sqrt(x+1)+sqrt(4*x+4)=sqrt(9*x+9))",
841 "solveFor x", "solutions L"];
842 val (dI',pI',mI') = ("RootEq",["univariate", "equation"],["no_met"]);
844 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
845 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
846 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
847 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
848 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
849 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
850 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
851 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
852 (*"13 + 13 * x + - 2 * sqrt ((4 + 4 * x) * (9 + 9 * x)) = 1 + x"
853 -> Subproblem ("RootEq", ["univariate", ...])*)
854 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
855 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
856 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
857 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
858 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
859 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
860 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
861 (*"144 + 288 * x + 144 * x \<up> 2 = 144 + x \<up> 2 + 288 * x + 143 * x \<up> 2"
862 -> Subproblem ("RootEq", ["univariate", ...])*)
863 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
864 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
865 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
866 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
867 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
868 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
869 if f = Form' (Test_Out.FormKF (~1, EdUndef, 0, Nundef, "0 = 0")) then ()
870 else error "rlang.sml: diff.behav. in Schalk II s.56 Bsp 73b";
871 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
872 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
873 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
874 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
875 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
876 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
877 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
878 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
879 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
880 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
881 val asm = Ctree.get_assumptions pt p;
882 if asm=[] andalso f = Form' (Test_Out.FormKF (~1,EdUndef,0,Nundef,"UniversalList")) andalso nxt = ("End_Proof'",End_Proof') then ()
883 else error "rlang.sml: diff.behav. in UniversalList 2";
885 (*----------------- Schalk II s.56 Bsp 74a ------------------------*)
886 "Schalk II s.56 Bsp 74a (sqrt(4*x+1) - sqrt(x+3) = sqrt(x - 2))";
887 "Schalk II s.56 Bsp 74a (sqrt(4*x+1) - sqrt(x+3) = sqrt(x - 2))";
888 "Schalk II s.56 Bsp 74a (sqrt(4*x+1) - sqrt(x+3) = sqrt(x - 2))";
890 val fmz = ["equality (sqrt(4*x+1) - sqrt(x+3) = sqrt(x - 2))",
891 "solveFor x", "solutions L"];
892 val (dI',pI',mI') = ("RootEq",["univariate", "equation"],["no_met"]);
894 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
895 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
896 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
897 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
898 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
899 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
900 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
901 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
902 (*4 + 5 * x + - 2 * sqrt (3 + 13 * x + 4 * x \<up> 2) = - 2 + x"
903 -> Subproblem ("RootEq", ["univariate", ...])*)
904 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
905 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
906 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
907 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
908 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
909 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
910 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
911 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
912 (*"12 + 52 * x + 16 * x \<up> 2 = 36 + x \<up> 2 + 48 * x + 15 * x \<up> 2"
913 -> Subproblem ("RootEq", ["univariate", ...])*)
914 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
915 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
916 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
917 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
918 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
919 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
920 if f = Form' (Test_Out.FormKF (~1, EdUndef, 0, Nundef, "- 24 + 4 * x = 0")) then ()
921 else error "rlang.sml: diff.behav. in Schalk II s.56 Bsp 74a";
922 (*-> ubproblem ("PolyEq", ["degree_1", ...]*)
923 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
924 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
925 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
926 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
927 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
928 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
929 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
930 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
931 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
932 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
933 case f of Form' (Test_Out.FormKF (~1,EdUndef,0,Nundef,"[x = 6]")) => ()
934 | _ => error "rlang.sml: diff.behav. in Schalk II s.56 Bsp 74a [x = 6]";
937 (*----------------- Schalk II s.56 Bsp 77b ------------------------*)
938 "Schalk II s.56 Bsp 77b (sqrt(x+12)+sqrt(x - 3) = sqrt(x + 32) - sqrt(5+x))";
939 "Schalk II s.56 Bsp 77b (sqrt(x+12)+sqrt(x - 3) = sqrt(x + 32) - sqrt(5+x))";
940 "Schalk II s.56 Bsp 77b (sqrt(x+12)+sqrt(x - 3) = sqrt(x + 32) - sqrt(5+x))";
942 val fmz = ["equality (sqrt(x+12)+sqrt(x - 3) = sqrt(x + 32) - sqrt(5+x))",
943 "solveFor x", "solutions L"];
944 val (dI',pI',mI') = ("RootEq",["univariate", "equation"],["no_met"]);
946 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
947 (* val nxt = ("Model_Problem",Model_Problem ["sq", "rootX", "univariate", "equation"]) *)
948 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
949 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
950 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
951 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
952 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
953 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
954 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
955 (* val nxt = ("Model_Problem",Model_Problem ["sq", "rootX", "univariate", "equation"]) *)
956 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
957 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
958 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
959 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
960 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
961 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
962 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; f2str f;
963 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
964 (* val nxt = ("Model_Problem",Model_Problem ["sq", "rootX", "univariate", "equation"]) *)
965 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
966 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
967 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
968 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
969 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
970 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
971 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
972 (*val nxt = ("Model_Problem",
973 Model_Problem ["normalise", "polynomial", "univariate", "equation"])*)
974 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
975 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
976 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
977 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
978 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
979 (*val (p,_,f,nxt,_,pt) = me nxt p [1] pt; since MGs norm_Rational*)
980 if f = Form'(Test_Out.FormKF (~1, EdUndef, 0, Nundef, "451584 + - 112896 * x = 0"))then()
981 else error "rlang.sml: diff.behav. in Schalk II s.56 Bsp 77b";
982 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
983 (* val nxt = ("Model_Problem",
984 Model_Problem ["degree_1", "polynomial", "univariate", "equation"])*)
985 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
986 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
987 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
988 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
989 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
990 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
991 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
992 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
993 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
994 case f of Form' (Test_Out.FormKF (~1,EdUndef,0,Nundef,"[]")) => ()
995 | _ => error "rlang.sml: diff.behav. in Schalk II s.56 Bsp 77b []";
996 (*added 040209 at introducing MGs norm_Rational ?!*)
997 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1000 (*----------------- Schalk II s.66 Bsp 4 ------------------------*)
1001 "Schalk II s.66 Bsp 4 ((6*x - 9)*(5*x+7) - (4*x+7)*(3*x - 6) = 429)";
1002 "Schalk II s.66 Bsp 4 ((6*x - 9)*(5*x+7) - (4*x+7)*(3*x - 6) = 429)";
1003 "Schalk II s.66 Bsp 4 ((6*x - 9)*(5*x+7) - (4*x+7)*(3*x - 6) = 429)";
1005 val fmz = ["equality ((6*x - 9)*(5*x+7) - (4*x+7)*(3*x - 6) = 429)",
1006 "solveFor x", "solutions L"];
1007 val (dI',pI',mI') = ("PolyEq",["univariate", "equation"],["no_met"]);
1008 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
1009 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1010 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1011 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1012 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1013 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1014 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1015 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1016 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1017 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1018 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1019 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1020 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1021 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1022 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1023 case f of Form' (Test_Out.FormKF (_,_,0,_,"[x = 5, x = -5]")) => ()
1024 | _ => error "rlang.sml: diff.behav. in Schalk II s.66 Bsp 4 []";
1027 (*----------------- Schalk II s.66 Bsp 8a ------------------------*)
1028 "Schalk II s.66 Bsp 8a ((x - 4)/(x+4) = (1 - x)/(1+x))";
1030 val fmz = ["equality ((x - 4)/(x+4) = (1 - x)/(1+x))",
1031 "solveFor x", "solutions L"];
1032 val (dI',pI',mI') = ("RatEq",["univariate", "equation"],["no_met"]);
1034 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
1035 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1036 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1037 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1038 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1039 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1040 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1041 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; f2str f;
1042 (*"(-4 + x) * (1 + x) = (1 + - 1 * x) * (4 + x)"
1043 -> Subproblem ("RatEq", ["univariate", ...])*)
1044 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1045 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1046 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1047 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1048 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1049 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;
1051 if f = Form' (Test_Out.FormKF (~1, EdUndef, 0, Nundef, "-8 + 2 * x \<up> 2 = 0")) then ()
1052 else error "rlang.sml: diff.behav. in Schalk II s.66 Bsp 8a";
1053 (*-> Subproblem ("PolyEq", ["polynomial", ...])*)
1055 val Form' (Test_Out.FormKF (~1, EdUndef, 0, Nundef, str)) = f;
1057 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1058 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1059 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1060 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1061 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1062 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1063 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1064 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1065 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1066 case f of Form' (Test_Out.FormKF (~1,EdUndef,0,Nundef,"[x = 2, x = - 2]")) => ()
1067 | _ => error "rlang.sml: diff.behav. in Schalk II s.66 Bsp 8a [x = 2, x = - 2]";
1069 (*----------------- Schalk II s.66 Bsp 10b ------------------------*)
1070 "Schalk II s.66 Bsp 10b (1/(x \<up> 2 - 9)+(2*x+3)/(x+3)=(3*x+4)/(x - 3))";
1071 "Schalk II s.66 Bsp 10b (1/(x \<up> 2 - 9)+(2*x+3)/(x+3)=(3*x+4)/(x - 3))";
1072 "Schalk II s.66 Bsp 10b (1/(x \<up> 2 - 9)+(2*x+3)/(x+3)=(3*x+4)/(x - 3))";
1073 val fmz = ["equality (1/(x \<up> 2 - 9)+(2*x+3)/(x+3)=(3*x+4)/(x - 3))",
1074 "solveFor x", "solutions L"];
1075 val (dI',pI',mI') = ("RatEq",["univariate", "equation"],["no_met"]);
1076 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
1077 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1078 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1079 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1080 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1081 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1082 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1083 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1084 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1085 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1086 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1087 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1088 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1095 "60 + 28 * x + - 13 * x \<up> 2 + - 1 * x \<up> 3 = 0")) then ()
1096 else error "rlang.sml: diff.behav. in Schalk II s.66 Bsp 10b";
1097 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 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1100 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1101 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1102 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1103 (*60 + 28 * x + - 13 * x \<up> 2 + - 1 * x \<up> 3 = 0 ... degree 3 not solvable*)
1106 (*----------------- Schalk II s.66 Bsp 20a ------------------------*)
1108 "Schalk II s.66 Bsp 20a (sqrt(29 - sqrt (x \<up> 2 - 9))=5)";
1109 "Schalk II s.66 Bsp 20a (sqrt(29 - sqrt (x \<up> 2 - 9))=5)";
1110 "Schalk II s.66 Bsp 20a (sqrt(29 - sqrt (x \<up> 2 - 9))=5)";
1111 val fmz = ["equality (sqrt(29 - sqrt(x \<up> 2 - 9))=5)",
1112 "solveFor x", "solutions L"];
1113 val (dI',pI',mI') = ("RootEq",["univariate", "equation"],["no_met"]);
1114 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
1115 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1116 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1117 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1118 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;
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;
1123 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1124 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1125 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1126 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1127 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1128 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1129 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1130 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1131 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1132 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1133 if f = Form' (Test_Out.FormKF (~1, EdUndef, 0, Nundef, "- 25 + x \<up> 2 = 0")) then ()
1134 else error "rlang.sml: diff.behav. in Schalk II s.66 Bsp 20a";
1135 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1136 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1137 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1138 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1139 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1140 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1141 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1142 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1143 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1144 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1145 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1146 case f of Form' (Test_Out.FormKF (~1,EdUndef,0,Nundef,"[x = 5, x = -5]")) => ()
1147 | _ => error "rlang.sml: diff.behav. in Schalk II s.66 Bsp 20a [x = 5, x = -5]";
1149 (*----------------- Schalk II s.66 Bsp 23b ------------------------*)
1150 "Schalk II s.66 Bsp 23b (2*sqrt(261 - x) - sqrt(2+2*x)=sqrt(2)*sqrt(5 - 3*x))";
1151 "Schalk II s.66 Bsp 23b (2*sqrt(261 - x) - sqrt(2+2*x)=sqrt(2)*sqrt(5 - 3*x))";
1152 "Schalk II s.66 Bsp 23b (2*sqrt(261 - x) - sqrt(2+2*x)=sqrt(2)*sqrt(5 - 3*x))";
1153 (*EO WN060310 something wrong:
1154 ([6, 6, 3, 1], Frm) "- 1064944 + 32 * x + -48 * x \<up> 2 = 0"
1156 ([6, 6, 3, 1], Res) "HOL.False"
1158 val fmz = ["equality (2*sqrt(261 - x) - sqrt(2+2*x)=sqrt(2)*sqrt(5 - 3*x))",
1159 "solveFor x", "solutions L"];
1160 val (dI',pI',mI') = ("RootEq",["univariate", "equation"],["no_met"]);
1162 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
1163 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1164 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1165 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1166 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1167 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1168 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1169 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1170 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1171 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1172 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1173 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1174 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1175 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1176 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1177 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1178 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1179 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1180 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1181 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1182 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; f2str f;
1185 (~1, EdUndef, 0, Nundef, "- 1064944 + 32 * x + -48 * x \<up> 2 = 0"))then()
1186 else error "rlang.sml: diff.behav. in Schalk II s.66 Bsp 23b";
1187 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1188 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1189 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1190 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1191 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1192 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1193 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1194 case f of Form' (Test_Out.FormKF (~1,EdUndef,_,Nundef,"[]")) => ()
1195 | _ => error "rlang.sml: diff.behav. in Schalk II s.66 Bsp 23b []";
1197 (*----------------- Schalk II s.66 Bsp 28a ------------------------*)
1198 "Schalk II s.66 Bsp 28a (A=(c/d)*sqrt(4*a \<up> 2 - c \<up> 2))";
1199 "Schalk II s.66 Bsp 28a (A=(c/d)*sqrt(4*a \<up> 2 - c \<up> 2))";
1200 "Schalk II s.66 Bsp 28a (A=(c/d)*sqrt(4*a \<up> 2 - c \<up> 2))";
1201 val fmz = ["equality (A=(c/d)*sqrt(4*a \<up> 2 - c \<up> 2))",
1202 "solveFor a", "solutions L"];
1203 val (dI',pI',mI') = ("RootEq",["univariate", "equation"],["no_met"]);
1204 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
1205 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1206 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1207 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1208 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1209 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1210 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1211 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1212 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1213 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1214 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1215 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1222 "c \<up> 4 / d \<up> 2 + A \<up> 2 * d \<up> 2 / d \<up> 2 +\n-4 * c \<up> 2 / d \<up> 2 * a \<up> 2 =\n0")) then ()*)
1224 "c \<up> 4 / d \<up> 2 + A \<up> 2 / 1 + -4 * c \<up> 2 / d \<up> 2 * a \<up> 2 = 0"
1225 then () else error "rlang.sml: diff.behav. in Schalk II s.66 Bsp 28a";
1226 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1227 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1228 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1229 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1230 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1231 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1232 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1233 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1234 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1235 case f of Form' (Test_Out.FormKF (~1,EdUndef,0,Nundef,"[a = sqrt ((c \<up> 4 + A \<up> 2 * d \<up> 2) / (4 * c \<up> 2)),\n a = - 1 * sqrt ((c \<up> 4 + A \<up> 2 * d \<up> 2) / (4 * c \<up> 2))]")) => ()
1236 | _ => error "rlang.sml: diff.behav. in Schalk II s.66 Bsp 28a [a=...]";
1240 (*----------------- Schalk II s.68 Bsp 52b ------------------------*)
1241 "Schalk II s.68 Bsp 52b (1/(x - a+b)=1/x - 1/a + 1/b)";
1242 val fmz = ["equality (1/(x - a+b)=1/x - 1/a + 1/b)",
1243 "solveFor x", "solutions L"];
1244 val (dI',pI',mI') = ("RatEq",["univariate", "equation"],["no_met"]);
1245 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
1246 (* val nxt = ("Model_Problem",Model_Problem ["rational", "univariate", "equation"])*)
1247 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1248 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1249 (*val nxt = ("Specify_Theory",Specify_Theory "RatEq")*)
1250 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1251 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1252 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1253 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1255 val f="1 * (a * (b * x)) = (a * b + (a * x + - 1 * (b * x))) * (b + (x + - 1 * a)
1256 val nxt = Subproblem ("RatEq",["univariate", "equation"]))*)
1257 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1258 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1259 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1260 (*val nxt = ("Specify_Theory",Specify_Theory "PolyEq")*)
1261 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1262 (* nxt = Specify_Problem ["normalise", "polynomial", "univariate", "equation"])*)
1263 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1264 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1265 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1266 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1267 (*val (p,_,f,nxt,_,pt) = me nxt p [1] pt; at introducing of MGs norm_Rational*)
1268 (*val p = ([4,5],Res) val f ="b * a \<up> 2 + - 1 * a * b \<up> 2 + (a \<up> 2 + b \<up> 2 + - 2 * a * b) * x +\n(b + - 1 * a) * x \<up> 2 =\n0"))
1269 val nxt = Subproblem ("PolyEq",["polynomial", "univariate", "equation"]))*)
1276 "b * a \<up> 2 + - 1 * a * b \<up> 2 + (a \<up> 2 + b \<up> 2 + - 2 * a * b) * x +\n(b + - 1 * a) * x \<up> 2 =\n0")) then ()
1277 else error "rlang.sml: diff.behav. in chalk I s.87 Bsp 38b";
1278 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1279 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1280 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1281 (*val nxt = ("Specify_Theory",Specify_Theory "PolyEq")*)
1282 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1283 (*Specify_Problem["abcFormula", "degree_2", "polynomial", "univariate", "equation*)
1284 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1285 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1286 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1287 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1288 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1289 (*val (p,_,f,nxt,_,pt) = me nxt p [1] pt;introducing MGs norm_Rational*)
1290 (*val p = ([4,6,5],Res) val f ="[x =\n (2 * a * b + - 1 * a \<up> 2 + - 1 * b \<up> 2 +\n sqrt\n (a \<up> 4 + b \<up> 4 + -4 * a * a * b \<up> 2 + -4 * a * b * a \<up> 2 +\n -4 * b * b * a \<up> 2 +\n 4 * a * a * b \<up> 2 +\n 4 * a * b * a \<up> 2 +\n 2 * a \<up> 2 * b \<up> 2)) /\n (- 2 * a + 2 * #"
1291 nx Check_Postcond["abcFormula", "degree_2", "polynomial", "univariate", "equation*)
1292 (*9.9.03: -"- ["normalise", "polynomial", "univar...*)
1293 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1294 (*val p = ([4,6],Res)
1295 val nxt =Check_Postcond ["normalise", "polynomial", "univariate", "equation"])*)
1296 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1297 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;(*1 additional for MGs norm_Rational*)
1298 if p = ([],Res) andalso f = Form' (Test_Out.FormKF (~1,EdUndef,0,Nundef,
1299 "[x =\n (2 * a * b + - 1 * a \<up> 2 + - 1 * b \<up> 2 +\n sqrt\n (a \<up> 4 + b \<up> 4 + -4 * a * a * b \<up> 2 + -4 * a * b * a \<up> 2 +\n -4 * b * b * a \<up> 2 +\n 4 * a * a * b \<up> 2 +\n 4 * a * b * a \<up> 2 +\n 2 * a \<up> 2 * b \<up> 2)) /\n (- 2 * a + 2 * b),\n x =\n (2 * a * b + - 1 * a \<up> 2 + - 1 * b \<up> 2 +\n - 1 *\n sqrt\n (a \<up> 4 + b \<up> 4 + -4 * a * a * b \<up> 2 + -4 * a * b * a \<up> 2 +\n -4 * b * b * a \<up> 2 +\n 4 * a * a * b \<up> 2 +\n 4 * a * b * a \<up> 2 +\n 2 * a \<up> 2 * b \<up> 2)) /\n (- 2 * a + 2 * b)]")) andalso nxt = ("End_Proof'",End_Proof') then writeln"simplify MG"
1300 else error "rlang.sml: diff.behav. in rational-a-b";
1302 (*----------------- Schalk II s.68 Bsp 56a ------------------------*)
1303 "Schalk II s.68 Bsp 56a ((a+b*x)/(a-b*x) - (a - b*x)/(a+b*x)= (4*a*b)/(a \<up> 2 - b \<up> 2))";
1304 val fmz = ["equality ((a+b*x)/(a-b*x) - (a - b*x)/(a+b*x)= (4*a*b)/(a \<up> 2 - b \<up> 2))", "solveFor x", "solutions L"];
1305 val (dI',pI',mI') = ("RatEq",["univariate", "equation"],["no_met"]);
1306 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
1307 (* val nxt = ("Model_Problem",Model_Problem ["rational", "univariate", "equation"]) *)
1308 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1309 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1310 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1311 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1312 (*SK loops with poly:
1313 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1314 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1317 (a + b * x) / (a + - 1 * (b * x)) + (- 1 * a + b * x) / (a + b * x) =
1318 4 * (a * b) / (a \<up> 2 + - 1 * b \<up> 2)
1319 add_fractions_p wird nicht angewendet, weil ...
1320 add_fract terminiert nicht: 030603
1321 siehe Rational.ML rational.sml
1325 "(a + b * x) / (a + - 1 * (b * x)) + - 1 * (a + - 1 * (b * x)) / (a + b * x) =\n4 * a * b / (a \<up> 2 + - 1 * b \<up> 2)"
1327 val nxt = ("Rewrite_Set",Rewrite_Set "make_ratpoly") : string * tac
1328 "(a + b * x) / (a + - 1 * b * x) + (- 1 * a + b * x) / (a + b * x) =\n4 *
1329 a * b / (a \<up> 2 + - 1 * b \<up> 2)"
1332 val t = TermC.parse_test @{context}"(a + b * x) / (a + - 1 * (b * x)) + - 1 * (a + - 1 * (b * x)) / (a + b * x) =\n4 * a * b / (a \<up> 2 + - 1 * b \<up> 2)";
1333 Rewrite.trace_on := false; (*true false*)
1334 val SOME (t',asm) = rewrite_set_ thy false norm_Rational t;
1336 Rewrite.trace_on:=false; (*true false*)
1338 # rls: norm_Rational on: (a + b * x) / (a + - 1 * (b * x)) + - 1 * (a + - 1 * (b * x)) / (a + b * x) = 4 * a * b / (a \<up> 2 + - 1 * b \<up> 2)
1340 ## rls: discard_minus on:
1342 ## rls: rat_mult_divide on:
1344 ## rls: reduce_0_1_2 on:
1345 ## rls: order_add_mult on:
1346 ### try thm: mult.commute
1347 === rewrites to: (a + b * x) / (a + - 1 * (b * x)) + (- 1 * a + - 1 * (- 1 * (b * x))) / (a + b * x) = b * (4 * a) / (a \<up> 2 + - 1 * b \<up> 2)
1349 ### try thm: real_mult_left_commute
1350 === rewrites to: (a + b * x) / (a + - 1 * (b * x)) + (- 1 * a + - 1 * (- 1 * (b * x))) / (a + b * x) = 4 * (b * a) / (a \<up> 2 + - 1 * b \<up> 2)
1352 ### try thm: mult.commute
1353 === rewrites to: (a + b * x) / (a + - 1 * (b * x)) + (- 1 * a + - 1 * (- 1 * (b * x))) / (a + b * x) = 4 * (a * b) / (a \<up> 2 + - 1 * b \<up> 2)
1356 === calc. to: (a + b * x) / (a + - 1 * (b * x)) + (- 1 * a + 1 * (b * x)) / (a +b * x) = 4 * (a * b) / (a \<up> 2 + - 1 * b \<up> 2)
1358 ## rls: add_fractions_p on: (a + b * x) / (a + - 1 * (b * x)) + (- 1 * a + 1 * (b * x)) / (a + b * x) =
1359 4 * (a * b) / (a \<up> 2 + - 1 * b \<up> 2)
1360 !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!GC
1362 ## rls: discard_minus on:
1364 ## rls: rat_mult_divide on:
1366 ## rls: reduce_0_1_2 on:
1367 ### try thm: real_mult_1
1368 === rewrites to: (a + b * x) / (a + - 1 * (b * x)) + (- 1 * a + b * x) / (a + b * x) = 4 * (a * b) / (a \<up> 2 + - 1 * b \<up> 2)
1370 ## rls: order_add_mult on:
1372 ## rls: add_fractions_p on: (a + b * x) / (a + - 1 * (b * x)) + (- 1 * a + b * x) / (a + b * x) =
1373 4 * (a * b) / (a \<up> 2 + - 1 * b \<up> 2)
1374 !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!GC
1376 ## rls: discard_minus on:
1378 ## rls: rat_mult_divide on:
1380 ## rls: reduce_0_1_2 on:
1381 ## rls: order_add_mult on:
1382 ## rls: collect_numerals on:
1383 ## rls: add_fractions_p on: (a + b * x) / (a + - 1 * (b * x)) + (- 1 * a + b * x) / (a + b * x) =
1384 4 * (a * b) / (a \<up> 2 + - 1 * b \<up> 2)
1385 !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!GC
1389 (*----------------- Schalk II s.68 Bsp 61b ------------------------*)
1390 "Schalk II s.68 Bsp 61b (sqrt(x+a)+sqrt(b - x)=sqrt(a+b))";
1391 val fmz = ["equality (sqrt(x+a)+sqrt(b - x)=sqrt(a+b))",
1392 "solveFor x", "solutions L"];
1393 val (dI',pI',mI') = ("RootEq",["univariate", "equation"],["no_met"]);
1395 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
1396 (* val nxt = ("Model_Problem",Model_Problem ["sq", "rootX", "univariate", "equation"])*)
1397 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1398 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1399 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1400 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1401 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1402 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1403 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1404 (* val nxt = ("Model_Problem",Model_Problem ["sq", "rootX", "univariate", "equation"])*)
1405 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1406 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1407 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1408 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1409 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1410 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1411 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1412 (*val nxt = ("Model_Problem",
1413 Model_Problem ["normalise", "polynomial", "univariate", "equation"])*)
1414 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1415 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1416 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1417 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1418 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1425 (*"-4 * b \<up> 2 + -4 * a * b + 4 * b \<up> 2 + 8 * a * b +\n(- 2 * a + -4 * a + -4 * b + 2 * a + 8 * b) * x +\n-4 * x \<up> 2 =\n0" before MG*)
1426 "4 * a * b + (-4 * a + 4 * b) * x + -4 * x \<up> 2 = 0")) then ()
1427 else error "rlang.sml: diff.behav. in Schalk II s.68 Bsp 61b";
1428 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1429 (*val nxt = ("Model_Problem", Model_Problem
1430 ["abcFormula", "degree_2", "polynomial", "univariate", "equation"])*)
1431 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1432 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1433 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1434 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1435 (* f= ... "-4 * b \<up> 2 + -4 * a * b + 4 * b \<up> 2 + 8 * a * b +
1436 (- 2 * a + -4 * a + -4 * b + 2 * a + 8 * b) * x + -4 * x \<up> 2 =0"*)
1437 (*val nxt = ("Rewrite_Set_Inst",Rewrite_Set_Inst ([#],"d2_polyeq_abcFormula_simplify"))*)
1438 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1439 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1440 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1441 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1442 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1443 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1444 (*if f = Form' (Test_Out.FormKF (~1,EdUndef,0,Nundef, with norm_Rational before MG
1445 "[x =\n (- 2 * a + -4 * b + 6 * a +\n sqrt\n (32 * a * b + - 16 * a \<up> 2 + -48 * b \<up> 2 + 24 * a \<up> 2 +\n 64 * b \<up> 2 +\n 8 * a \<up> 2)) /\n -8,\n x =\n (- 2 * a + -4 * b + 6 * a +\n - 1 *\n sqrt\n (32 * a * b + - 16 * a \<up> 2 + -48 * b \<up> 2 + 24 * a \<up> 2 +\n 64 * b \<up> 2 +\n 8 * a \<up> 2)) /\n -8]")) then writeln"simplify MG"*)
1446 if f = Form' (Test_Out.FormKF (~1,EdUndef,0,Nundef,"[x =\n (-4 * b + 4 * a + sqrt (32 * a * b + 16 * a \<up> 2 + 16 * b \<up> 2)) / -8,\n x =\n (-4 * b + 4 * a + - 1 * sqrt (32 * a * b + 16 * a \<up> 2 + 16 * b \<up> 2)) /\n -8]")) then ()
1447 else error "rlang.sml: diff.behav. Bsp 61b";
1448 (*WN.18.12.03: extreme run-time !!!*)
1451 (*----------------- Schalk II s.68 Bsp 62b ------------------------*)
1452 "Schalk II s.68 Bsp 62b (sqrt((x+a) \<up> 2+(x - 2*b) \<up> 2)=a+2*b)";
1453 val fmz = ["equality (sqrt((x+a) \<up> 2+(x - 2*b) \<up> 2)=a+2*b)",
1454 "solveFor x", "solutions L"];
1455 val (dI',pI',mI') = ("RootEq",["univariate", "equation"],["no_met"]);
1456 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
1457 (*val nxt = ("Model_Problem",Model_Problem ["sq", "rootX", "univariate", "equation"]) *)
1458 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1459 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1460 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1461 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1462 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1463 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1464 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1465 (* val nxt = ("Model_Problem",
1466 Model_Problem ["normalise", "polynomial", "univariate", "equation"])*)
1467 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1468 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1469 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1470 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1471 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1478 "-4 * a * b + (-4 * b + 2 * a) * x + 2 * x \<up> 2 = 0")) then ()
1479 else error "rlang.sml: diff.behav. in Schalk II s.68 Bsp 62b";
1480 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1481 (*val nxt = ("Model_Problem", Model_Problem
1482 ["abcFormula", "degree_2", "polynomial", "univariate", "equation"])*)
1483 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1484 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1485 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1486 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1487 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1488 (*val f = ... "-4 * a * b + (-4 * b + 2 * a) * x + 2 * x \<up> 2 = 0" *)
1489 (*val nxt = ("Rewrite_Set_Inst",Rewrite_Set_Inst ([#],"d2_polyeq_abcFormula_simplify"))*)
1490 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1491 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1492 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1493 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1494 (*val (p,_,f,nxt,_,pt) = me nxt p [1] pt;introduc.MGs norm_Rational*)
1495 if f = Form' (Test_Out.FormKF (~1,EdUndef,0,Nundef,
1496 "[x = (- 2 * a + 4 * b + sqrt (16 * a * b + 16 * b \<up> 2 + 4 * a \<up> 2)) / 4,\n x =\n (- 2 * a + 4 * b + - 1 * sqrt (16 * a * b + 16 * b \<up> 2 + 4 * a \<up> 2)) / 4]")) then writeln "simplify MG"
1497 else error "rlang.sml: diff.behav. in II 62b [x=...]";
1498 val asms = Ctree.get_assumptions pt p;
1499 if asms = [TermC.parse_test @{context}"0 <= ((- 2 * a + 4 * b + sqrt (16 * a * b + 16 * b \<up> 2 + 4 * a \<up> 2)) / 4 + a) \<up> 2 + ((- 2 * a + 4 * b + sqrt (16 * a * b + 16 * b \<up> 2 + 4 * a \<up> 2)) / 4 - 2 * b) \<up> 2",
1500 TermC.parse_test @{context}"0 <= a + 2 * b",
1501 TermC.parse_test @{context}"8 * (-4 * a * b) <= (-4 * b + 2 * a) \<up> 2",
1502 TermC.parse_test @{context}"8 * (-4 * a * b) <= (-4 * b + 2 * a) \<up> 2",
1503 TermC.parse_test @{context}"0 <= ((- 2 * a + 4 * b + - 1 * sqrt (16 * a * b + 16 * b \<up> 2 + 4 * a \<up> 2)) / 4 + a) \<up> 2 + ((- 2 * a + 4 * b + - 1 * sqrt (16 * a * b + 16 * b \<up> 2 + 4 * a \<up> 2)) / 4 - 2 * b) \<up> 2",
1504 TermC.parse_test @{context}"0 <= a + 2 * b",
1505 TermC.parse_test @{context}"8 * (-4 * a * b) <= (-4 * b + 2 * a) \<up> 2",
1506 TermC.parse_test @{context}"8 * (-4 * a * b) <= (-4 * b + 2 * a) \<up> 2"]
1507 then writeln "should be simplified MG"
1508 else error "rlang.sml: diff.behav. in II 62b asms";
1510 "------ WN.TEST---------------------------------";
1511 "------ WN.TEST---------------------------------";
1512 "------ WN.TEST---------------------------------";
1514 val fmz = ["equality ((2*x+1)*x \<up> 2 = 0)",
1515 "solveFor x", "solutions L"];
1516 val (dI',pI',mI') = ("PolyEq",["univariate", "equation"],["no_met"]);
1517 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
1518 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1519 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1520 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1521 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1522 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1524 val f = Form' (Test_Out.FormKF (~1,EdUndef,1,Nundef,"(2 * x + 1) * x \<up> 2 = 0"))
1525 normiert nicht ... korr.WN:
1526 val t = TermC.parse_test @{context} "(2*x+1)*x \<up> 2 = 0";
1527 val subst = [(TermC.parse_test @{context} "bdv", TermC.parse_test @{context} "x")];
1528 val SOME (t',_) = rewrite_set_inst_ thy false subst make_ratpoly_in t;
1529 if UnparseC.term t' = "x \<up> 2 + 2 * x \<up> 3 = 0" then ()
1530 else error "rlang.sml: 7";
1532 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1533 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1534 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1535 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1536 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1538 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1539 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1540 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1541 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1542 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1543 if f = Form' (Test_Out.FormKF (~1,EdUndef,0,Nundef,"[x = 0, x = 0, x = - 1 / 2]")) then()
1544 else error "rlang.sml WN.TEST new behaviour";
1546 "------ rlang.sml end---------------------------------";
1548 (*------------------------------vvv-Rewrite_Set "rat_eliminate"---------
1549 > Rewrite.trace_on:=true; (*true false*)
1550 > val t = TermC.parse_test @{context}
1551 "(3 + - 1 * x + 1 * x \<up> 2) / (9 * x + -6 * x \<up> 2 + 1 * x \<up> 3) = 1 / x";
1552 > val SOME (t',asm) =
1553 rewrite_ thy dummy_ord rateq_erls true rat_mult_denominator_both t;
1554 > UnparseC.term t'; UnparseC.terms asm;
1555 "(3 + - 1 * x + 1 * x \<up> 2) * x = 1 * (9 * x + -6 * x \<up> 2 + 1 * x \<up> 3)"
1556 "[\"9 * x + -6 * x \<up> 2 + 1 * x \<up> 3 ~= 0\",\"x ~= 0\"]"
1557 > Rewrite.trace_on:=false; (*true false*)
1558 ------------------------------ \<up> -Rewrite_Set "rat_eliminate"---------*)
1561 "-------------------- WN.15.5.03: Pythagoras -------------------------------";
1562 "-------------------- WN.15.5.03: Pythagoras -------------------------------";
1563 "-------------------- WN.15.5.03: Pythagoras -------------------------------";
1565 val fmz = ["equality ((a/2) \<up> 2 + (b/2) \<up> 2 = r \<up> 2)",
1566 "solveFor a", "solutions L"];
1567 val (dI',pI',mI') = ("PolyEq",["univariate", "equation"],["no_met"]);
1568 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
1569 (* Model_Problem ["normalise", "polynomial", "univariate", "equation"])*)
1570 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1571 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1572 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1573 val (p,_,f,nxt,_,pt) = me nxt p c pt;
1574 (*val nxt = ("Apply_Method",Apply_Method ["PolyEq", "normalise_poly"])*)
1575 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1576 val (p,_,f,nxt,_,pt) = me nxt p c pt;
1577 (*val nxt = Subproblem ("PolyEq",["polynomial", "univariate", "equation"])*)
1578 val (p,_,f,nxt,_,pt) = me nxt p c pt;
1579 val (p,_,f,nxt,_,pt) = me nxt p c pt;
1580 (*val nxt =Model_Problem ["sq_only", "degree_2", "polynomial", "univariate", "equation"])*)
1581 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1582 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1583 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1584 val (p,_,f,nxt,_,pt) = me nxt p c pt;
1585 (*val nxt = Apply_Method ["PolyEq", "solve_d2_polyeq_sqonly_equation"])*)
1586 val (p,_,f,nxt,_,pt) = me nxt p c pt;
1587 val (p,_,f,nxt,_,pt) = me nxt p c pt;
1588 val (p,_,f,nxt,_,pt) = me nxt p c pt;
1589 val (p,_,f,nxt,_,pt) = me nxt p c pt;
1590 val (p,_,f,nxt,_,pt) = me nxt p c pt;
1591 val (p,_,f,nxt,_,pt) = me nxt p c pt;
1592 val (p,_,f,nxt,_,pt) = me nxt p c pt;
1593 if f = Form' (Test_Out.FormKF (~1,EdUndef,0,Nundef,
1594 "[a = sqrt ((- 1 * b \<up> 2 + 4 * r \<up> 2) / 1),\n a = - 1 * sqrt ((- 1 * b \<up> 2 + 4 * r \<up> 2) / 1)]")) andalso nxt = ("End_Proof'",End_Proof')
1595 then writeln"simplify result\nsimplify result\nsimplify result"
1596 else error "rlang.sml: diff.behav. in Pythagoras";
1597 val asms = Ctree.get_assumptions pt p;
1598 (*if asms = [TermC.parse_test @{context}"0 <= -4 * (b \<up> 2 / 4 + -4 * r \<up> 2 / 4)",
1599 TermC.parse_test @{context}"0 <= -4 * (b \<up> 2 / 4 + -4 * r \<up> 2 / 4)"]*)
1600 if UnparseC.terms (*WN1104changed*) asms =
1601 "[0 <= -4 * (b \<up> 2 / 4 + - 1 * r \<up> 2 / 1),\
1602 \0 <= -4 * (b \<up> 2 / 4 + - 1 * r \<up> 2 / 1)]"
1603 then writeln"simplify result\nsimplify result\nsimplify result"
1604 else error "rlang.sml: diff.behav. in Pythagoras asms";
1607 "-------------------- WN.15.5.03: equation within the maximum example ------";
1608 "-------------------- WN.15.5.03: equation within the maximum example ------";
1609 "-------------------- WN.15.5.03: equation within the maximum example ------";
1611 val fmz = ["equality (2*sqrt(r \<up> 2 - (u/2) \<up> 2) - u \<up> 2/(2*sqrt(r \<up> 2 - (u/2) \<up> 2))= 0)",
1612 "solveFor u", "solutions L"];
1613 val (dI',pI',mI') = ("PolyEq",["univariate", "equation"],["no_met"]);
1615 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
1616 (* Model_Problem ["normalise", "rootX", "univariate", "equation"])*)
1617 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1618 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1619 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1620 val (p,_,f,nxt,_,pt) = me nxt p c pt;
1621 (*val nxt = Apply_Method ["RootEq", "norm_sq_root_equation"]) *)
1622 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1623 (*val nxt = Subproblem ("RootEq",["univariate", "equation"]))*)
1624 val (p,_,f,nxt,_,pt) = me nxt p c pt;
1625 (*val nxt = Model_Problem ["sq", "rootX", "univariate", "equation"]) *)
1626 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1627 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1628 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1629 val (p,_,f,nxt,_,pt) = me nxt p c pt;
1630 (*val nxt = Apply_Method ["RootEq", "solve_sq_root_equation"]) *)
1631 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1632 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1633 val (p,_,f,nxt,_,pt) = me nxt p c pt;
1634 (*val nxt = Subproblem ("RootEq",["univariate", "equation"]))*)
1635 val (p,_,f,nxt,_,pt) = me nxt p c pt;
1636 (*val nxt = Model_Problem ["rational", "univariate", "equation"]) *)
1637 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1638 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1639 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1640 val (p,_,f,nxt,_,pt) = me nxt p c pt;
1641 (*val nxt = Apply_Method ["RootEq", "solve_rat_equation"]) *)
1642 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1643 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1644 (*val nxt = Subproblem ("RootEq",["univariate", "equation"]))*)
1645 val (p,_,f,nxt,_,pt) = me nxt p c pt;
1646 (*val nxt = Model_Problem ["normalise", "polynomial", "univariate", "equation"]) *)
1647 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1648 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1649 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1650 val (p,_,f,nxt,_,pt) = me nxt p c pt;
1651 (*val nxt = Apply_Method ["PolyEq", "normalise_poly"]) *)
1652 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1653 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1654 (*val nxt = Subproblem ("PolyEq",["polynomial", "univariate", "equation"]))*)
1661 "- 16 * r \<up> 4 + 8 * r \<up> 2 * u \<up> 2 = 0")) then ()
1662 else error "rlang.sml: diff.behav. in Schalk I s.87 Bsp 38b";
1663 val (p,_,f,nxt,_,pt) = me nxt p c pt;
1664 (*val nxt = Model_Problem ["sq_only", "degree_2", "polynomial", "univariate", "equation"]) *)
1665 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1666 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1667 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1668 val (p,_,f,nxt,_,pt) = me nxt p c pt;
1669 (*val nxt = Apply_Method ["PolyEq", "solve_d2_polyeq_sqonly_equation"]) *)
1670 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1671 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1672 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1673 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1674 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1675 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1676 val (p,_,f,nxt,_,pt) = me nxt p c pt;
1677 if f = Form' (Test_Out.FormKF (~1,EdUndef,0,Nundef,"[u = sqrt (2 * r \<up> 2 / 1), u = - 1 * sqrt (2 * r \<up> 2 / 1)]")) then()
1678 else error "rlang.sml WN.TEST new behaviour in max-rooteq";