|
neuper@37906
|
1 |
(* testexamples for RootratEq, equations mixing fractions and roots
|
|
neuper@37906
|
2 |
use"rootrateq.sml";
|
|
neuper@37906
|
3 |
*)
|
|
neuper@37906
|
4 |
|
|
neuper@41943
|
5 |
|
|
neuper@41943
|
6 |
"--------------------- tests on predicates -------------------------------";
|
|
neuper@41943
|
7 |
"--------------------- tests on predicates -------------------------------";
|
|
neuper@41943
|
8 |
"--------------------- tests on predicates -------------------------------";
|
|
neuper@41943
|
9 |
|
|
neuper@41943
|
10 |
(*=== inhibit exn ?=============================================================
|
|
neuper@41943
|
11 |
|
|
neuper@38050
|
12 |
val thy = (theory "Isac");
|
|
neuper@37906
|
13 |
|
|
neuper@37906
|
14 |
(*
|
|
neuper@37906
|
15 |
Compiler.Control.Print.printDepth:=5; (*4 default*)
|
|
neuper@37906
|
16 |
trace_rewrite:=true;
|
|
neuper@37906
|
17 |
trace_rewrite:=false;
|
|
neuper@37906
|
18 |
*)
|
|
neuper@37906
|
19 |
val t1 = (term_of o the o (parse thy)) "(-8 - sqrt(x) + x^^^2) is_rootRatAddTerm_in x";
|
|
neuper@37926
|
20 |
val SOME (t,_) = rewrite_set_ RootRatEq.thy false RootRatEq_prls t1;
|
|
neuper@41928
|
21 |
if (term2str t) = "HOL.False" then ()
|
|
neuper@38031
|
22 |
else error "rootrateq.sml: diff.behav. 1 in is_rootRatAddTerm_in";
|
|
neuper@37906
|
23 |
|
|
neuper@37906
|
24 |
val t1 = (term_of o the o (parse thy)) "(1/x) is_rootRatAddTerm_in x";
|
|
neuper@37926
|
25 |
val SOME (t,_) = rewrite_set_ RootRatEq.thy false RootRatEq_prls t1;
|
|
neuper@41928
|
26 |
if (term2str t) = "HOL.False" then ()
|
|
neuper@38031
|
27 |
else error "rootrateq.sml: diff.behav. 2 in is_rootRatAddTerm_in";
|
|
neuper@37906
|
28 |
|
|
neuper@37906
|
29 |
val t1 = (term_of o the o (parse thy)) "(1/sqrt(x)) is_rootRatAddTerm_in x";
|
|
neuper@37926
|
30 |
val SOME (t,_) = rewrite_set_ RootRatEq.thy false RootRatEq_prls t1;
|
|
neuper@41928
|
31 |
if (term2str t) = "HOL.False" then ()
|
|
neuper@38031
|
32 |
else error "rootrateq.sml: diff.behav. 3 in is_rootRatAddTerm_in";
|
|
neuper@37906
|
33 |
|
|
neuper@37906
|
34 |
val t1 = (term_of o the o (parse thy)) "(1/(sqrt(x)+1)) is_rootRatAddTerm_in x";
|
|
neuper@37926
|
35 |
val SOME (t,_) = rewrite_set_ RootRatEq.thy false RootRatEq_prls t1;
|
|
neuper@41928
|
36 |
if (term2str t) = "HOL.True" then ()
|
|
neuper@38031
|
37 |
else error "rootrateq.sml: diff.behav. 4 in is_rootRatAddTerm_in";
|
|
neuper@37906
|
38 |
|
|
neuper@37906
|
39 |
val t1 = (term_of o the o (parse thy)) "(3 + 1/(1+sqrt(x))) is_rootRatAddTerm_in x";
|
|
neuper@37926
|
40 |
val SOME (t,_) = rewrite_set_ RootRatEq.thy false RootRatEq_prls t1;
|
|
neuper@41928
|
41 |
if (term2str t) = "HOL.True" then ()
|
|
neuper@38031
|
42 |
else error "rootrateq.sml: diff.behav. 5 in is_rootRatAddTerm_in";
|
|
neuper@37906
|
43 |
|
|
neuper@37906
|
44 |
val t1 = (term_of o the o (parse thy)) "(1/(1+sqrt(y)) + 3 + 1/(1+sqrt(x))) is_rootRatAddTerm_in x";
|
|
neuper@37926
|
45 |
val SOME (t,_) = rewrite_set_ RootRatEq.thy false RootRatEq_prls t1;
|
|
neuper@41928
|
46 |
if (term2str t) = "HOL.True" then ()
|
|
neuper@38031
|
47 |
else error "rootrateq.sml: diff.behav. 6 in is_rootRatAddTerm_in";
|
|
neuper@37906
|
48 |
|
|
neuper@37906
|
49 |
val t1 = (term_of o the o (parse thy)) "(1/(1+sqrt(x)) + 3 + 1/(1+sqrt(y))) is_rootRatAddTerm_in x";
|
|
neuper@37926
|
50 |
val SOME (t,_) = rewrite_set_ RootRatEq.thy false RootRatEq_prls t1;
|
|
neuper@41928
|
51 |
if (term2str t) = "HOL.True" then ()
|
|
neuper@38031
|
52 |
else error "rootrateq.sml: diff.behav. 7 in is_rootRatAddTerm_in";
|
|
neuper@37906
|
53 |
|
|
neuper@37906
|
54 |
|
|
neuper@37906
|
55 |
"--------------------- test thm rootrat_equation_left_1 ---------------------";
|
|
neuper@37906
|
56 |
val fmz = ["equality ( -2 + 1/(1 - sqrt(x))= 0)", "solveFor x","solutions L"];
|
|
neuper@37991
|
57 |
val (dI',pI',mI') = ("RootRatEq",["univariate","equation"],["no_met"]);
|
|
neuper@37906
|
58 |
|
|
neuper@37906
|
59 |
val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
|
|
neuper@37906
|
60 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
|
neuper@37906
|
61 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
|
neuper@37906
|
62 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
|
neuper@37906
|
63 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
|
neuper@37906
|
64 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
|
neuper@37906
|
65 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
|
neuper@37991
|
66 |
(*-> Subproblem ("RootEq", ["univariate", ...])*)
|
|
neuper@37906
|
67 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
|
neuper@37906
|
68 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
|
neuper@37906
|
69 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
|
neuper@37906
|
70 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
|
neuper@37906
|
71 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
|
neuper@37906
|
72 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
|
neuper@37991
|
73 |
(*-> Subproblem ("RootEq", ["univariate", ...])*)
|
|
neuper@37906
|
74 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
|
neuper@37906
|
75 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
|
neuper@37906
|
76 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
|
neuper@37906
|
77 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
|
neuper@37906
|
78 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
|
neuper@37906
|
79 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
|
neuper@37991
|
80 |
(*-> Subproblem ("RootEq", ["univariate", ...])*)
|
|
neuper@37906
|
81 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
|
neuper@37906
|
82 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
|
neuper@37906
|
83 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
|
neuper@37906
|
84 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
|
neuper@37906
|
85 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
|
neuper@37906
|
86 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
|
neuper@37906
|
87 |
if f = Form' (FormKF (~1, EdUndef, 0, Nundef, "1 + -4 * x = 0")) then ()
|
|
neuper@38031
|
88 |
else error "rootrateq.sml: diff.behav. in rootrat_equation_left_1";
|
|
neuper@37991
|
89 |
(*-> Subproblem ("RootEq", ["polynomial", ...])*)
|
|
neuper@37906
|
90 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
|
neuper@37906
|
91 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
|
neuper@37906
|
92 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
|
neuper@37906
|
93 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
|
neuper@37906
|
94 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
|
neuper@37906
|
95 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
|
neuper@37906
|
96 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
|
neuper@37906
|
97 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
|
neuper@37906
|
98 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
|
neuper@37906
|
99 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
|
neuper@37906
|
100 |
case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 1 / 4]")) => ()
|
|
neuper@38031
|
101 |
| _ => error "rootrateq.sml: diff.behav. in -2 + 1/(1 - sqrt(x))= 0 -> [x = 1/4]";
|
|
neuper@37906
|
102 |
|
|
neuper@37906
|
103 |
"--------------------- test thm rootrat_equation_left_2 ---------------------";
|
|
neuper@37906
|
104 |
val fmz = ["equality (3/(1+sqrt(x))= 1)", "solveFor x","solutions L"];
|
|
neuper@37991
|
105 |
val (dI',pI',mI') = ("RootRatEq",["univariate","equation"],["no_met"]);
|
|
neuper@37906
|
106 |
|
|
neuper@37906
|
107 |
val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
|
|
neuper@37906
|
108 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
|
neuper@37906
|
109 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
|
neuper@37906
|
110 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
|
neuper@37906
|
111 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
|
neuper@37906
|
112 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
|
neuper@37991
|
113 |
(*-> Subproblem ("RootEq", ["univariate", ...])*)
|
|
neuper@37906
|
114 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
|
neuper@37906
|
115 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
|
neuper@37906
|
116 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
|
neuper@37906
|
117 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
|
neuper@37906
|
118 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
|
neuper@37906
|
119 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
|
neuper@37991
|
120 |
(*-> Subproblem ("RootEq", ["univariate", ...])*)
|
|
neuper@37906
|
121 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
|
neuper@37906
|
122 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
|
neuper@37906
|
123 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
|
neuper@37906
|
124 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
|
neuper@37906
|
125 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
|
neuper@37906
|
126 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
|
neuper@37991
|
127 |
(*-> Subproblem ("RootEq", ["univariate", ...])*)
|
|
neuper@37906
|
128 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
|
neuper@37906
|
129 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
|
neuper@37906
|
130 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
|
neuper@37906
|
131 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
|
neuper@37906
|
132 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
|
neuper@37906
|
133 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
|
neuper@37906
|
134 |
if f = Form' (FormKF (~1, EdUndef, 0, Nundef, "4 + -1 * x = 0")) then ()
|
|
neuper@38031
|
135 |
else error "rootrateq.sml: diff.behav. in rootrat_equation_left_2";
|
|
neuper@37991
|
136 |
(*-> Subproblem ("PolyEq", ["polynomial", ...])*)
|
|
neuper@37906
|
137 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
|
neuper@37906
|
138 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
|
neuper@37906
|
139 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
|
neuper@37906
|
140 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
|
neuper@37906
|
141 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
|
neuper@37906
|
142 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
|
neuper@37906
|
143 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
|
neuper@37906
|
144 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
|
neuper@37906
|
145 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
|
neuper@37906
|
146 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
|
neuper@37906
|
147 |
case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 4]")) => ()
|
|
neuper@38031
|
148 |
| _ => error "rootrateq.sml: diff.behav. in 3/(1+sqrt(x))= 1 -> [x = 4]";
|
|
neuper@37906
|
149 |
|
|
neuper@37906
|
150 |
"--------------------- test thm rootrat_equation_right_1 ---------------";
|
|
neuper@37906
|
151 |
val fmz = ["equality ( 0= -2 + 1/(1 - sqrt(x)))", "solveFor x","solutions L"];
|
|
neuper@37991
|
152 |
val (dI',pI',mI') = ("RootRatEq",["univariate","equation"],["no_met"]);
|
|
neuper@37906
|
153 |
|
|
neuper@37906
|
154 |
val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
|
|
neuper@37906
|
155 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
|
neuper@37906
|
156 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
|
neuper@37906
|
157 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
|
neuper@37906
|
158 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
|
neuper@37906
|
159 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
|
neuper@37906
|
160 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
|
neuper@37906
|
161 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
|
neuper@37906
|
162 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
|
neuper@37906
|
163 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
|
neuper@37906
|
164 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
|
neuper@37906
|
165 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
|
neuper@37906
|
166 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
|
neuper@37906
|
167 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
|
neuper@37906
|
168 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
|
neuper@37906
|
169 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
|
neuper@37906
|
170 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
|
neuper@37906
|
171 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
|
neuper@37906
|
172 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
|
neuper@37906
|
173 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
|
neuper@37906
|
174 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
|
neuper@37906
|
175 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
|
neuper@37906
|
176 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
|
neuper@37906
|
177 |
if f = Form' (FormKF (~1, EdUndef, 0, Nundef, "-1 + 4 * x = 0")) then ()
|
|
neuper@38031
|
178 |
else error "rootrateq.sml: diff.behav.ppoly in rootrat_equation_right_1";
|
|
neuper@37906
|
179 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
|
neuper@37906
|
180 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
|
neuper@37906
|
181 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
|
neuper@37906
|
182 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
|
neuper@37906
|
183 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
|
neuper@37906
|
184 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
|
neuper@37906
|
185 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
|
neuper@37906
|
186 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
|
neuper@37906
|
187 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
|
neuper@37906
|
188 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
|
neuper@37906
|
189 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
|
neuper@37906
|
190 |
case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 1 / 4]")) => ()
|
|
neuper@38031
|
191 |
| _ => error "rootrateq.sml: diff.behav. in -2 + 1/(1 - sqrt(x))= 0 -> [x = 1/4]";
|
|
neuper@37906
|
192 |
|
|
neuper@37906
|
193 |
"--------------------- test thm rootrat_equation_right_2 --------------------";
|
|
neuper@37906
|
194 |
val fmz = ["equality (1 = 3/(1+sqrt(x)))", "solveFor x","solutions L"];
|
|
neuper@37991
|
195 |
val (dI',pI',mI') = ("RootRatEq",["univariate","equation"],["no_met"]);
|
|
neuper@37906
|
196 |
|
|
neuper@37906
|
197 |
val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
|
|
neuper@37906
|
198 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
|
neuper@37906
|
199 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
|
neuper@37906
|
200 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
|
neuper@37906
|
201 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
|
neuper@37906
|
202 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
|
neuper@37906
|
203 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
|
neuper@37906
|
204 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
|
neuper@37906
|
205 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
|
neuper@37906
|
206 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
|
neuper@37906
|
207 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
|
neuper@37906
|
208 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
|
neuper@37906
|
209 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
|
neuper@37906
|
210 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
|
neuper@37906
|
211 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
|
neuper@37906
|
212 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
|
neuper@37906
|
213 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
|
neuper@37906
|
214 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
|
neuper@37906
|
215 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
|
neuper@37906
|
216 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
|
neuper@37906
|
217 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
|
neuper@37906
|
218 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
|
neuper@37906
|
219 |
if f = Form' (FormKF (~1, EdUndef, 0, Nundef, "-4 + x = 0")) then ()
|
|
neuper@38031
|
220 |
else error "rootrateq.sml: diff.behav. in rootrat_equation_right_2";
|
|
neuper@37906
|
221 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
|
neuper@37906
|
222 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
|
neuper@37906
|
223 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
|
neuper@37906
|
224 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
|
neuper@37906
|
225 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
|
neuper@37906
|
226 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
|
neuper@37906
|
227 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
|
neuper@37906
|
228 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
|
neuper@37906
|
229 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
|
neuper@37906
|
230 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
|
neuper@37906
|
231 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
|
neuper@37906
|
232 |
case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 4]")) => ()
|
|
neuper@38031
|
233 |
| _ => error "rootrateq.sml: diff.behav. in 3/(1+sqrt(x))= 1 -> [x = 4]";
|
|
neuper@41943
|
234 |
===== inhibit exn ?===========================================================*)
|