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