1 (* Title: "Knowledge/rateq.sml"
2 Author: Richard Lang 2009
3 (c) copyright due to lincense terms.
6 "-----------------------------------------------------------------";
7 "table of contents -----------------------------------------------";
8 "-----------------------------------------------------------------";
9 "----------- pbl: rational, univariate, equation ----------------";
10 "----------- solve (1/x = 5, x) by me ---------------------------";
11 "----------- S.68, Bsp.: 40, ((x)/(x - 8) + (x - 8)/(x) = 26/5)--";
12 "----------- x / (x ^ 2 - 6 * x + 9) - 1 / (x ^ 2 - 3 * x) = 1 /x";
13 "----------- ((5*x)/(x - 2) - x/(x+2)=(4::real)), incl. refine ---------------------------------";
14 "-----------------------------------------------------------------";
15 "-----------------------------------------------------------------";
17 val thy = @{theory "RatEq"};
18 val ctxt = Proof_Context.init_global thy;
20 "------------ pbl: rational, univariate, equation ----------------";
21 "------------ pbl: rational, univariate, equation ----------------";
22 "------------ pbl: rational, univariate, equation ----------------";
23 val t = ParseC.parse_test ctxt "(1/b+1/x=1) is_ratequation_in x";
24 val SOME (t_, _) = rewrite_set_ ctxt false RatEq_prls t;
25 val result = UnparseC.term @{context} t_;
26 if result <> "True" then error "rateq.sml: new behaviour 1:" else ();
28 val t = ParseC.parse_test ctxt "(sqrt(x)=1) is_ratequation_in x";
29 val SOME (t_, _) = rewrite_set_ ctxt false RatEq_prls t;
30 val result = UnparseC.term @{context} t_;
31 if result <> "False" then error "rateq.sml: new behaviour 2:" else ();
33 val t = ParseC.parse_test ctxt "(x=- 1) is_ratequation_in x";
34 val SOME (t_,_) = rewrite_set_ ctxt false RatEq_prls t;
35 val result = UnparseC.term @{context} t_;
36 if result <> "False" then error "rateq.sml: new behaviour 3:" else ();
38 val t = ParseC.parse_test ctxt "(3 + x \<up> 2 + 1/(x \<up> 2+3)=1) is_ratequation_in x";
39 val SOME (t_,_) = rewrite_set_ ctxt false RatEq_prls t;
40 val result = UnparseC.term @{context} t_;
41 if result <> "True" then error "rateq.sml: new behaviour 4:" else ();
43 val result = M_Match.by_formalise ["equality (x=(1::real))", "solveFor x", "solutions L"]
44 (Problem.from_store @{context} ["rational", "univariate", "equation"]);
45 case result of M_Match.NoMatch' _ => () | _ => error "rateq.sml: new behaviour: 5";
47 val result = M_Match.by_formalise ["equality (3 + x \<up> 2 + 1/(x \<up> 2+3)=1)", "solveFor x", "solutions L"]
48 (Problem.from_store @{context} ["rational", "univariate", "equation"]);
49 case result of M_Match.Matches' _ => () | _ => error "rateq.sml: new behaviour: 6";
51 "------------ solve (1/x = 5, x) by me ---------------------------";
52 "------------ solve (1/x = 5, x) by me ---------------------------";
53 "------------ solve (1/x = 5, x) by me ---------------------------";
54 val fmz = ["equality (1/x=(5::real))", "solveFor x", "solutions L"];
56 ((** )"RatEq"( **)"PolyEq"(*rls "make_ratpoly_in" missing in theory "RatEq" (and ancestors)*),
57 ["univariate", "equation"],["no_met"]);
58 val (p,_,f,nxt,_,pt) = Test_Code.init_calc @{context} [(fmz, (dI',pI',mI'))];
59 (* val (p,_,f,nxt,_,pt) = me nxt p [1] pt;------------- now Refine_Tacitly*)
60 (* nxt = ("Model_Problem",Model_Problem ["rational", "univariate", "equation"]) *)
61 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
62 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
63 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
64 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
66 case nxt of (Rewrite_Set "RatEq_eliminate") => () | _ => ((*not checked before*));
67 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
69 WN120317.TODO dropped rateq: here "x ~= 0 should TermC.sub_at to ctxt, but it does not:
70 --- repair NO asms from rls RatEq_eliminate --- shows why.
71 so it needs more effort to find out, how Check_elementwise worked in 2002, see below.
74 (* val nxt = (_,Subproblem ("RatEq",["univariate", "equation"] ======= *)
75 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
76 (* val (p,_,f,nxt,_,pt) = me nxt p [1] pt;------------- now Refine_Tacitly*)
77 (*val nxt = ("Model_Problem", Model_Problem ["normalise", "polynomial", "univariate", "equation"])*)
78 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
79 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
80 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
81 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
82 (*val nxt = Apply_Method ["PolyEq", "normalise_poly"])*)
83 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
84 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
85 (* val nxt = (_,Subproblem ("PolyEq",["polynomial", "univariate", "equation"]=======*)
86 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
87 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
88 (* ("Model_Problem", Model_Problem ["degree_1", "polynomial", "univariate", "equation"])*)
89 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
90 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
91 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
92 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
93 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
94 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
95 val (p''',_,f,nxt''',_,pt''') = me nxt p [1] pt;
96 f2str f = "[x = 1 / 5]";
97 case nxt of (Check_elementwise "Assumptions") => () | _ => ((*not checked before*));
98 "~~~~~ fun me, args:"; val (tac, (p:pos'), _, (pt:ctree)) = (nxt, p, c, pt);
99 val (pt, p) = case Step.by_tactic tac (pt,p) of
100 ("ok", (_, _, ptp)) => ptp | _ => error "--- solve (1/x = 5.. Step.by_tactic";
101 "~~~~~ fun Step.do_next, args:"; val (ip as (_,p_), (ptp as (pt,p), tacis)) = (p, ((pt, e_pos'), []))
102 val pIopt = get_pblID (pt,ip); (*= SOME ["rational", "univariate", "equation"]
103 1- 1 associated to metID ["RatEq", "solve_rat_equation"]*)
105 member op = [Pbl,Met] p_; (*= false*)
106 "~~~~~ fun do_next, args:"; val (ptp as (pt, pos as (p, p_))) = (pt, ip);
107 val thy' = get_obj g_domID pt (par_pblobj pt p);
108 val (is, sc) = resume_prog (p,p_) pt; (*is: which ctxt?*)
109 "~~~~~ fun find_next_step, args:"; val () = ();
110 (*----- outcommented during cleanup of args in lucas-interpreter.sml ------------------------\\* )
111 "~~~~~ fun go_scan_up, args:"; val (thy, ptp, (Prog sc), E, l, ay, a, v) =
112 (thy, ptp, sc, E, l, true, a, v);
113 1 < length l; (*true*)
114 val up = drop_last l;
115 TermC.sub_at up sc; (* = Const (\<^const_name>\<open>Let\<close>, *)
116 "~~~~~ fun scan_up, args:"; val (thy, ptp, (program as (Prog sc)), E, l, ay,
117 (t as Const (\<^const_name>\<open>Let\<close>,_) $ _), a, v) = (thy, ptp, (Prog sc), E, up, ay, (TermC.sub_at up sc), a, v);
118 ay = Napp_; (*false*)
119 val up = drop_last l;
120 val (Const (\<^const_name>\<open>Let\<close>,_) $ e $ (Abs (i,T,body))) = TermC.sub_at up sc; (*Const (\<^const_name>\<open>SubProblem\<close>,..*)
121 val i = mk_Free (i, T);
122 val E = Env.update E (i, v);
123 "~~~~~ fun scan_dn, args:"; val ((thy as (th,sr)), (pt, p), E, l, t, a, v) =
124 (thy, ptp, E, (up@[R,D]), body, a, v);
125 "~~~~~ fun check_leaf, args:"; val (call, thy, prog_rls, (E, (a, v)), t) = ("next ", th, sr, (E, (a, v)), t);
126 "~~~~~ fun eval_leaf, args:"; val (E, a, v,
127 (t as (Const (\<^const_name>\<open>Check_elementwise\<close>,_) $ _ $ _ ))) = (E, a, v, t);
128 val Program.Tac tm = Program.Tac (subst_atomic E t);
129 UnparseC.term @{context} tm = "Check_elementwise [x = 1 / 5] {v_v. Assumptions}";
130 (* ------ \<up> ----- ? "x" ?*)
131 "~~~~~ to check_leaf return val:"; val ((Program.Tac stac, a')) = ((Program.Tac (subst_atomic E t), NONE));
132 val stac' = eval_prog_expr (ThyC.get_theory @{context} thy) prog_rls (subst_atomic (upd_env_opt E (a,v)) stac);
133 UnparseC.term @{context} stac' = "Check_elementwise [x = 1 / 5] {v_v. Assumptions}";
134 "~~~~~ to scan_dn return val:"; val ((a', Program.Tac stac)) = ((a', Program.Tac stac'));
135 val m = LItool.tac_from_prog pt (ThyC.get_theory @{context} th) stac;
136 case m of Check_elementwise "Assumptions" => () | _ => (); (*m' = Empty_Tac_ ???!??? *);
137 val (p''''', pt''''', m''''') = (p, pt, m);
138 "~~~~~ fun check , args:"; val ((p,p_), pt, (m as Check_elementwise pred)) = (p, pt, m);
139 member op = [Pbl,Met] p_; (* = false*)
140 val pp = par_pblobj pt p;
141 val thy' = (get_obj g_domID pt pp):theory';
142 val thy = ThyC.get_theory @{context} thy'
143 val metID = (get_obj g_metID pt pp)
144 val {crls,...} = MethodC.from_store ctxt metID
145 val (f,asm) = case p_ of Frm => (get_obj g_form pt p , [])
146 | Res => get_obj g_result pt p;
147 UnparseC.term @{context} f = "[x = 1 / 5]"; (*the current formula*)
148 val vp = (Proof_Context.init_global thy, pred) |-> ParseC.term_opt |> the |> mk_set thy pt p f;
149 val (bdv, asms) = vp;
151 UnparseC.term @{context} bdv = "x";
152 UnparseC.terms @{context} asms = (* asms from rewriting are missing : vvv *)
153 ("[\"~ (matches (?a = 0) (1 = 5 * x)) | ~ lhs (1 = 5 * x) is_poly_in x\",\"x = 1 / 5\", " ^
154 "\"lhs (1 + -5 * x = 0) is_poly_in x\",\"lhs (1 + -5 * x = 0) has_degree_in x = 1\", " ^
155 "\"1 / x = 5 is_ratequation_in x\"]");
157 WN120317.TODO dropped rateq: ctxt should contain "x ~= 0 here, but it does not, see above.
160 val Applicable.Yes (Check_elementwise' (curr_form, pred, (res, asms))) = check p''''' pt''''' m''''';
161 UnparseC.term @{context} curr_form = "[x = 1 / 5]";
162 pred = "Assumptions";
163 res = ParseC.parse_test @{context} "[]::bool list";
166 val (p,_,f,nxt,_,pt) = me nxt''' p''' [] pt'''; (*<<<----- this caused the error*)
168 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
170 if p = ([], Res) andalso f2str f = "[x = 1 / 5]"
171 then case nxt of ("End_Proof'", End_Proof') => ()
172 | _ => error "rateq.sml: new behaviour: [x = 1 / 5] 1"
173 else error "rateq.sml: new behaviour: [x = 1 / 5] 2";
174 ( *----- outcommented during cleanup of args in lucas-interpreter.sml ------------------------//*)
176 "------------ S.68, Bsp.: 40, ((x)/(x - 8) + (x - 8)/(x) = 26/5)--";
177 "------------ S.68, Bsp.: 40, ((x)/(x - 8) + (x - 8)/(x) = 26/5)--";
178 "------------ S.68, Bsp.: 40, ((x)/(x - 8) + (x - 8)/(x) = 26/5)--";
179 (*EP Schalk_II_p68_n40*)
180 val fmz = ["equality ((x)/(x - 8) + (x - 8)/(x) = 26/(5::real))", "solveFor x", "solutions L"];
182 ((** )"RatEq"( **)"PolyEq"(*rls "make_ratpoly_in" missing in theory "RatEq" (and ancestors)*),
183 ["univariate", "equation"],["no_met"]);
184 val (p,_,f,nxt,_,pt) = Test_Code.init_calc @{context} [(fmz, (dI',pI',mI'))];
185 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
186 (* nxt = ("Model_Problem",Model_Problem ["rational", "univariate", "equation"])*)
187 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
188 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
189 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
190 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
191 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
192 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
193 (* nxt = ("Subproblem",Subproblem ("RatEq",["univariate", "equation"]))*)
194 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
195 (* nxt = ("Model_Problem", Model_Problem ["normalise", "polynomial", "univariate", "equation"])*)
196 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
197 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
198 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
199 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
200 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
202 if p = ([4, 3], Pbl) then ()
205 (Add_Given "equality (320 + 128 * x + - 16 * x \<up> 2 = 0)") =>
207 Test_Out.PpcKF (Test_Out.Problem [], {
208 Find = [Incompl "solutions []"], Given = [Incompl "equality", Incompl "solveFor"],
209 Relate = [], Where = [P_Model.False "matches (?a + ?v_ \<up> 2 = 0) e_e \<or>\nmatches (?a + ?b * ?v_ \<up> 2 = 0) e_e"],
211 | _ => error ("S.68, Bsp.: 40 PblObj changed"))
212 | _ => error ("S.68, Bsp.: 40 changed nxt =" ^ Tactic.input_to_string ctxt nxt));
214 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
215 (* ("Subproblem", Subproblem ("PolyEq",["polynomial", "univariate", "equation"])) *)
216 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
217 (* nxt = ("Model_Problem", Model_Problem
218 ["abcFormula", "degree_2", "polynomial", "univariate", "equation"])*)
219 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
220 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
221 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
222 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
223 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
224 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
225 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
226 if p = ([], Res) andalso f2str f = "[x = - 2, x = 10]" then ()
227 else error "rateq.sml: new behaviour: [x = - 2, x = 10]";
230 "----------- ((5*x)/(x - 2) - x/(x+2)=(4::real)), incl. refine ---------------------------------";
231 "----------- ((5*x)/(x - 2) - x/(x+2)=(4::real)), incl. refine ---------------------------------";
232 "----------- ((5*x)/(x - 2) - x/(x+2)=(4::real)), incl. refine ---------------------------------";
233 (*was in test/../usecases.sml*)
234 val fmz = ["equality ((5*x)/(x - 2) - x/(x+2)=(4::real))", "solveFor x", "solutions L"];
236 ((** )"RatEq"( **)"PolyEq"(*rls "make_ratpoly_in" missing in theory "RatEq" (and ancestors)*),
237 ["univariate", "equation"],["no_met"]);
238 val (p,_,f,nxt,_,pt) = Test_Code.init_calc @{context} [(fmz, (dI',pI',mI'))];
239 (*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [1] pt; val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
240 (**)val (p,_,f,nxt,_,pt) = me nxt p [1] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;(**)
241 (**)val (p,_,f,nxt,_,pt) = me nxt p [1] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;(**)
242 (*[], Met*)val (p,_,f,nxt,_,pt) = me nxt p [1] pt;(*Apply_Method ["RatEq", "solve_rat_equation"]*)
243 (*[1], Frm*)val (p,_,f,nxt,_,pt) = me nxt p [] pt;(*Rewrite_Set "RatEq_simplify":*)
245 (*+*)if (get_istate_LI pt p |> Istate.string_of ctxt) (* still specify-phase: found_accept = false ---------------------------------> vvvvv*)
246 (*+*) = "Pstate ([\"\n(e_e, 5 * x / (x - 2) - x / (x + 2) = 4)\", \"\n(v_v, x)\"], [], empty, NONE, \n??.empty, ORundef, false, true)"
247 (*+*)then () else error "rat-eq + subpbl: istate in specify-phase";
249 (*[1], Res*)val (p,_,f,nxt,_,pt) = me nxt p [1] pt;(*Rewrite_Set "norm_Rational"*)
251 (*+*)if (get_istate_LI pt p |> Istate.string_of ctxt) (* solve-phase: found_accept = true -----------------------------------------------------------------------------------------------> vvvvv*)
252 (*+*) = "Pstate ([\"\n(e_e, 5 * x / (x - 2) - x / (x + 2) = 4)\", \"\n(v_v, x)\"], [R, L, R, L, L, R, R, R], empty, SOME e_e, \n5 * x / (x + - 1 * 2) + - 1 * x / (x + 2) = 4, ORundef, true, true)"
253 (*+*)then () else error "rat-eq + subpbl: istate after found_accept";
255 (*[2], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt;(*Rewrite_Set "RatEq_eliminate"*)
258 (*[3], Res*)val (p,_,f,nxt,_,pt) = me nxt p [1] pt;(*Subproblem ("PolyEq", ["normalise", "polynomial", "univariate", "equation"])*)
259 (*[4], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt;(*Model_Problem*)
261 (**)val (p,_,f,nxt,_,pt) = me nxt p [1] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;(**)
262 (**)val (p,_,f,nxt,_,pt) = me nxt p [1] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;(**)
263 (**)val (p,_,f,nxt,_,pt) = me nxt p [1] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;(**)
264 (**)val (p,_,f,nxt,_,pt) = me nxt p [1] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;(**)
266 (**)val (p,_,f,nxt,_,pt) = me nxt p [1] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;(**)
267 (**)val (p,_,f,nxt,_,pt) = me nxt p [1] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;(**)
268 (**)val (p,_,f,nxt,_,pt) = me nxt p [1] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;(**)
269 (**)val (p,_,f,nxt,_,pt) = me nxt p [1] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;(**)
271 (*[4,4], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [1] pt;(*Specify_Problem ["degree_1", "polynomial", "univariate", "equation"]*)
272 (*[4,4], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [1] pt;(*Specify_Method ["PolyEq", "solve_d1_polyeq_equation"]*)
274 (*[4,4], Met*)val (p,_,f,nxt,_,pt) = me nxt p [1] pt;(*Apply_Method ["PolyEq", "solve_d1_polyeq_equation"]*)
275 (*[4,4,1], Frm*)val (p,_,f,nxt,_,pt) = me nxt p [1] pt;(*Rewrite_Set_Inst (["(''bdv'', x)"], "d1_polyeq_simplify")*)
276 (*[4,4,1], Res*)val (p,_,f,nxt,_,pt) = me nxt p [1] pt;(*Rewrite_Set "polyeq_simplify"*)
277 (*[4,4,2], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt;(*Or_to_List*)
278 (* f = Test_Out.FormKF "[x = -4 / 3]" *)
279 (*[4,4,3], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt;(*Check_elementwise "Assumptions"*)
280 (*[4,4,4], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt;(*Check_Postcond ["degree_1", "polynomial", "univariate", "equation"]*)
281 (*[4,4], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt;(*Check_Postcond ["normalise", "polynomial", "univariate", "equation"]*)
282 (*[4], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt;(*Check_elementwise "Assumptions"*)
283 (*[5], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt;(*Check_Postcond ["rational", "univariate", "equation"]*)
284 (*[], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt;(*End_Proof'*)
286 if p = ([], Res) andalso f2str f = "[x = - 4 / 3]"
287 then case nxt of End_Proof' => () | _ => error "rat-eq + subpbl: end CHANGED 1"
288 else error "rat-eq + subpbl: end CHANGED 2";