1.1 --- a/test/Tools/isac/IsacKnowledge/rooteq.sml Mon Aug 30 14:29:49 2010 +0200
1.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
1.3 @@ -1,470 +0,0 @@
1.4 -(* RL 10.02
1.5 - use"../kbtest/rooteq.sml";
1.6 - use"rooteq.sml";
1.7 - testexamples for RootEq, equations with fractions
1.8 -
1.9 - Compiler.Control.Print.printDepth:=10; (*4 default*)
1.10 - Compiler.Control.Print.printDepth:=5; (*4 default*)
1.11 - trace_rewrite:=true;
1.12 -*)
1.13 -"----------- rooteq.sml begin--------";
1.14 -"--------------(1/sqrt(x)=5)---------------------------------------";
1.15 -"--------------(4*sqrt(4*x+2)=3*sqrt(2*x+24))----------------------";
1.16 -"--------------(sqrt(x+1)=5)---------------------------------------";
1.17 -"--------------(sqrt(x+1)+sqrt(4*x+4)=sqrt(9*x+9))-----------------";
1.18 -"--------------(3*sqrt(x+3)+sqrt(x+6)=sqrt(4*x+33))----------------";
1.19 -"--------------(sqrt(x+1)+sqrt(4*x+4)=sqrt(9*x+9))-----------------";
1.20 -
1.21 -val t = (term_of o the o (parse RootEq.thy)) "(sqrt(2+x+3)) is_rootTerm_in x";
1.22 -val SOME(t_, _) = rewrite_set_ RootEq.thy false RootEq_prls t;
1.23 -val result = term2str t_;
1.24 -if result <> "True" then raise error "rooteq.sml: new behaviour:" else ();
1.25 -
1.26 -val t = (term_of o the o (parse RootEq.thy)) "(sqrt(2+x+3)) is_rootTerm_in x";
1.27 -val SOME(t_, _) = rewrite_set_ RootEq.thy false RootEq_prls t;
1.28 -val result = term2str t_;
1.29 -if result <> "True" then raise error "rooteq.sml: new behaviour:" else ();
1.30 -
1.31 -val t = (term_of o the o (parse RootEq.thy)) "(nroot 5 (x+4)) is_rootTerm_in x";
1.32 -val SOME(t_, _) = rewrite_set_ RootEq.thy false RootEq_prls t;
1.33 -val result = term2str t_;
1.34 -if result <> "True" then raise error "rooteq.sml: new behaviour:" else ();
1.35 -
1.36 -val t = (term_of o the o (parse RootEq.thy)) "(sqrt(2+x+3)) is_sqrtTerm_in x";
1.37 -val SOME(t_, _) = rewrite_set_ RootEq.thy false RootEq_prls t;
1.38 -val result = term2str t_;
1.39 -if result <> "True" then raise error "rooteq.sml: new behaviour:" else ();
1.40 -
1.41 -val t = (term_of o the o (parse RootEq.thy)) "(sqrt(25)) is_sqrtTerm_in x";
1.42 -val SOME(t_, _) = rewrite_set_ RootEq.thy false RootEq_prls t;
1.43 -val result = term2str t_;
1.44 -if result <> "False" then raise error "rooteq.sml: new behaviour:" else ();
1.45 -
1.46 -val t = (term_of o the o (parse RootEq.thy)) "sqrt(1 + x) is_normSqrtTerm_in x";
1.47 -val SOME(t_, _) = rewrite_set_ RootEq.thy false RootEq_prls t;
1.48 -val result = term2str t_;
1.49 -if result <> "True" then raise error "rooteq.sml: new behaviour:" else ();
1.50 -
1.51 -val t = (term_of o the o (parse RootEq.thy)) "(3+3*sqrt(x)) is_normSqrtTerm_in x";
1.52 -val SOME(t_, _) = rewrite_set_ RootEq.thy false RootEq_prls t;
1.53 -val result = term2str t_;
1.54 -if result <> "True" then raise error "rooteq.sml: new behaviour:" else ();
1.55 -
1.56 -val t = (term_of o the o (parse RootEq.thy)) "(sqrt(x+1)+1) is_normSqrtTerm_in x";
1.57 -val SOME(t_, _) = rewrite_set_ RootEq.thy false RootEq_prls t;
1.58 -val result = term2str t_;
1.59 -if result <> "False" then raise error "rooteq.sml: new behaviour:" else ();
1.60 -
1.61 -val t = (term_of o the o (parse RootEq.thy)) "(1 - u/(sqrt(r - u))) is_normSqrtTerm_in u";
1.62 -val SOME(t_, _) = rewrite_set_ RootEq.thy false RootEq_prls t;
1.63 -val result = term2str t_;
1.64 -if result <> "False" then raise error "rooteq.sml: new behaviour:" else ();
1.65 -
1.66 -val t = (term_of o the o (parse RootEq.thy)) "(x*(1+x)/(sqrt(x+1))) is_normSqrtTerm_in x";
1.67 -val SOME(t_, _) = rewrite_set_ RootEq.thy false RootEq_prls t;
1.68 -val result = term2str t_;
1.69 -if result <> "True" then raise error "rooteq.sml: new behaviour:" else ();
1.70 -
1.71 -val t = (term_of o the o (parse RootEq.thy)) "(1 - (sqrt(2+x+3)^^^3)) is_normSqrtTerm_in x";
1.72 -val SOME(t_, _) = rewrite_set_ RootEq.thy false RootEq_prls t;
1.73 -val result = term2str t_;
1.74 -if result <> "False" then raise error "rooteq.sml: new behaviour:" else ();
1.75 -
1.76 -val t = (term_of o the o (parse RootEq.thy)) "(1 + (sqrt(2+x+3)^^^3)) is_normSqrtTerm_in x";
1.77 -val SOME(t_, _) = rewrite_set_ RootEq.thy false RootEq_prls t;
1.78 -val result = term2str t_;
1.79 -if result <> "True" then raise error "rooteq.sml: new behaviour:" else ();
1.80 -
1.81 -
1.82 -
1.83 -val result = match_pbl ["equality (sqrt(x)=1)","solveFor x","solutions L"]
1.84 - (get_pbt ["root","univariate","equation"]);
1.85 -case result of Matches' _ => () | _ => raise error "rooteq.sml: new behaviour:";
1.86 -
1.87 -val result = match_pbl ["equality (sqrt(25)=1)","solveFor x","solutions L"]
1.88 - (get_pbt ["root","univariate","equation"]);
1.89 -case result of NoMatch' _ => () | _ => raise error "rooteq.sml: new behaviour:";
1.90 -
1.91 -(*---------rooteq---- 23.8.02 ---------------------*)
1.92 -"---------(1/sqrt(x)=5)---------------------";
1.93 -val fmz = ["equality (1/sqrt(x)=5)","solveFor x","solutions L"];
1.94 -val (dI',pI',mI') = ("RootEq.thy",["univariate","equation"],["no_met"]);
1.95 -
1.96 -val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
1.97 -val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.98 -val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.99 -val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.100 -val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.101 -val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.102 -val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.103 -(*"1 / x = 25" -> Subproblem ("RootEq.thy", ["univariate", ...]) *)
1.104 -val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.105 -val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.106 -val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.107 -val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.108 -val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.109 -val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.110 -(*"1 = 25 * x" -> Subproblem ("RatEq.thy", ["univariate", ...])*)
1.111 -val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.112 -val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.113 -val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.114 -val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.115 -val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.116 -val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.117 -if f = Form' (FormKF (~1, EdUndef, 0, Nundef, "1 + -25 * x = 0")) then ()
1.118 -else raise error "rooteq.sml: diff.behav.poly in (1/sqrt(x)=5)";
1.119 -(*-> Subproblem ("PolyEq.thy", ["polynomial", ...])*)
1.120 -val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.121 -val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.122 -val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.123 -val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.124 -val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.125 -val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.126 -val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.127 -val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.128 -val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.129 -val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.130 -val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.131 -case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 1 / 25]")) => ()
1.132 - | _ => raise error "rooteq.sml: diff.behav. [x = 1 / 25]";
1.133 -if asms2str (get_assumptions_ pt p) = "[(0 <= 1 / 25, [])]"
1.134 -(*WN050916 before correction 'rewrite__set_ called with 'Erls' for ..:
1.135 - [(str2term"25 ~= 0",[])] *)
1.136 -then writeln "should be True\n\
1.137 - \should be True\n\
1.138 - \should be True\n"
1.139 -else raise error "rooteq.sml: diff.behav. with 25 ~= 0";
1.140 -
1.141 -"---------(sqrt(x+1)=5)---------------------";
1.142 -val fmz = ["equality (sqrt(x+1)=5)","solveFor x","solutions L"];
1.143 -val (dI',pI',mI') = ("RootEq.thy",["univariate","equation"],["no_met"]);
1.144 -(*val p = e_pos';
1.145 -val c = [];
1.146 -val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
1.147 -val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
1.148 -val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
1.149 -val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.150 -val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.151 -val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.152 -val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.153 -val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.154 -val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.155 -(*-> Subproblem ("RootEq.thy", ["univariate", ...])*)
1.156 -val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.157 -val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.158 -val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.159 -val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.160 -val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.161 -val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.162 -if f = Form' (FormKF (~1, EdUndef, 0, Nundef, "-24 + x = 0")) then ()
1.163 -else raise error "rooteq.sml: diff.behav.poly in sqrt(x+1)=5";
1.164 -(*-> Subproblem ("PolyEq.thy", ["polynomial", ...])*)
1.165 -val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.166 -val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.167 -val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.168 -val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.169 -val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.170 -val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.171 -val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.172 -val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.173 -val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.174 -case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 24]")) => ()
1.175 - | _ => raise error "rooteq.sml: diff.behav. [x = 24]";
1.176 -
1.177 -"-------------(4*sqrt(4*x+2)=3*sqrt(2*x+24))-----------------";
1.178 -val fmz = ["equality (4*sqrt(4*x+2)=3*sqrt(2*x+24))","solveFor x","solutions L"];
1.179 -val (dI',pI',mI') = ("RootEq.thy",["univariate","equation"],["no_met"]);
1.180 -
1.181 -val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
1.182 -val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.183 -val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.184 -val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.185 -val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.186 -val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.187 -val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.188 -val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.189 -val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.190 -val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.191 -val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.192 -val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.193 -if f = Form' (FormKF (~1, EdUndef, 0, Nundef, "-184 + 46 * x = 0")) then ()
1.194 -else raise error "rooteq.sml: diff.behav.poly in 4*sqrt(4*x+2)=3*sqrt(2*x+24)";
1.195 -val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.196 -val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.197 -val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.198 -val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.199 -val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.200 -val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.201 -val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.202 -val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.203 -val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.204 -case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 4]")) => ()
1.205 - | _ => raise error "rooteq.sml: diff.behav. [x = 4]";
1.206 -if get_assumptions_ pt p = [(str2term"0 <= 12 * sqrt 2 * 4",[])]
1.207 -then writeln "should be True\nshould be True\nshould be True\n\
1.208 - \should be True\nshould be True\nshould be True\n"
1.209 -else raise error "rooteq.sml: diff.behav. with 0 <= 12 * sqrt 2 * 4";
1.210 -
1.211 -"--------------(sqrt(x+1)+sqrt(4*x+4)=sqrt(9*x+9))----------------";
1.212 -val fmz = ["equality (sqrt(x+1)+sqrt(4*x+4)=sqrt(9*x+9))","solveFor x","solutions L"];
1.213 -val (dI',pI',mI') = ("RootEq.thy",["univariate","equation"],["no_met"]);
1.214 -
1.215 -val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
1.216 -(*val nxt = Model_Problem ["sq","root","univariate","equation"]) *)
1.217 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.218 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.219 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.220 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.221 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.222 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.223 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.224 -(*"13 + 13 * x + -2 * sqrt ((4 + 4 * x) * (9 + 9 * x)) = 1 + x"))
1.225 -val nxt = ("Subproblem",Subproblem ("RootEq.thy",["univariate","equation"]))*)
1.226 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.227 -(*val nxt = Model_Problem ["sq","root","univariate","equation"]) *)
1.228 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.229 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.230 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.231 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.232 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.233 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.234 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.235 -(*"144 + 288 * x + 144 * x ^^^ 2 = 144 + x ^^^ 2 + 288 * x + 143 * x ^^^ 2"))
1.236 -val nxt = ("Subproblem",Subproblem ("RootEq.thy",["univariate","equation"]))*)
1.237 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.238 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.239 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.240 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.241 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.242 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.243 -if f = Form' (FormKF (~1, EdUndef, 0, Nundef, "0 = 0")) then ()
1.244 -else raise error "rooteq.sml: diff.behav.poly in (sqrt(x+1)+sqrt(4*x+4)=sqr..";
1.245 -(*-> Subproblem ("PolyEq.thy", ["degree_0", ...])*)
1.246 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.247 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.248 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.249 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.250 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.251 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.252 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.253 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.254 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.255 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.256 -val asm = get_assumptions_ pt p;
1.257 -if f = Form' (FormKF (~1,EdUndef,0,Nundef,"UniversalList")) andalso asm = []
1.258 -then () else raise error "rooteq.sml: diff.behav. in UniversalList 1";
1.259 -
1.260 -
1.261 -
1.262 -"--------------(sqrt(x+1)+sqrt(4*x+4)=sqrt(9*x+9))---------- SUBPBL.2.------";
1.263 -val fmz =
1.264 - ["equality (13 + 13 * x + -2 * sqrt ((4 + 4 * x) * (9 + 9 * x)) = 1 + x)",
1.265 - "solveFor x","solutions L"];
1.266 -val (dI',pI',mI') = ("RootEq.thy",["sq","root","univariate","equation"],
1.267 - ["RootEq","solve_sq_root_equation"]);
1.268 -(*val p = e_pos'; val c = [];
1.269 -val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
1.270 -val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
1.271 -val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
1.272 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.273 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.274 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.275 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.276 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.277 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.278 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.279 -(*"144 + 288 * x + 144 * x ^^^ 2 = 144 + x ^^^ 2 + 288 * x + 143 * x ^^^ 2"))
1.280 -val nxt = ("Subproblem",Subproblem ("RootEq.thy",["univariate","equation"])) *)
1.281 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.282 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.283 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.284 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.285 -(*val p = ([6],Pbl)val nxt = Specify_Method ["PolyEq","normalize_poly"])*)
1.286 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.287 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.288 -(*val p = ([6,2],Res) val f = Form' (FormKF (~1,EdUndef,2,Nundef,"0 = 0"))
1.289 -val nxt = Subproblem ("PolyEq.thy",["polynomial","univariate","equation"]))*)
1.290 -if f = Form' (FormKF (~1, EdUndef, 0, Nundef, "0 = 0")) then ()
1.291 -else raise error "rooteq.sml: diff.behav.poly in sqrt(x+1)+sqrt(4*x+4)=sqrt..";
1.292 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.293 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.294 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.295 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.296 -(*val nxt = Specify_Method ["PolyEq","solve_d0_polyeq_equation"]) *)
1.297 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.298 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.299 -(*val p = ([6,3,1],Res) val f = Form' (FormKF (~1,EdUndef,3,Nundef,"True"))
1.300 -val nxt = ("Or_to_List",Or_to_List) : string * tac*)
1.301 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.302 -(*val p = ([6,3,2],Res) val f = (~1,EdUndef,3,Nundef,"UniversalList"))
1.303 -val nxt = Check_Postcond ["degree_0","polynomial","univariate","equation"])*)
1.304 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.305 -(*val p = ([6,3],Res) val f =(~1,EdUndef,2,Nundef,"UniversalList"))
1.306 -val nxt = Check_Postcond ["normalize","polynomial","univariate","equation"])*)
1.307 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.308 -if f = Form' (FormKF (~1, EdUndef, 0, Nundef, "UniversalList")) then ()
1.309 -else raise error "rooteq.sml: diff.behav.poly in sqrt(x+1)+sqrt(4*x+4)=sqrt..";
1.310 -(* val Form' (FormKF (~1, EdUndef, 0, Nundef, str)) = f;
1.311 - *)
1.312 -
1.313 -(*same error as full expl #######*)
1.314 -
1.315 -"--------------(sqrt(x+1)+sqrt(4*x+4)=sqrt(9*x+9))---------- OKversion----";
1.316 -val fmz = ["equality (sqrt(x) = 1)","solveFor x","solutions L"];
1.317 -val (dI',pI',mI') = ("RootEq.thy",["sq","root","univariate","equation"],
1.318 - ["RootEq","solve_sq_root_equation"]);
1.319 -(*val p = e_pos'; val c = [];
1.320 -val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
1.321 -val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
1.322 -val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
1.323 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.324 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.325 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.326 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.327 -(*val p = ([],Pbl)val nxt = Specify_Method ["RootEq","solve_sq_root_equation"*)
1.328 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.329 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.330 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.331 -(* val p = ([2],Res) val f = Form' (FormKF (~1,EdUndef,1,Nundef,"x = 1"))
1.332 -val nxt = ("Subproblem",Subproblem ("RootEq.thy",["univariate","equation"]))*)
1.333 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.334 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.335 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.336 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.337 -(*val nxt = ("Specify_Method",Specify_Method ["PolyEq","normalize_poly"])*)
1.338 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.339 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.340 -(*val p = ([3,2],Res)val f = Form' (FormKF (~1,EdUndef,2,Nundef,"-1 + x = 0"))
1.341 -val nxt = Subproblem ("PolyEq.thy",["polynomial","univariate","equation"]))*)
1.342 -if f = Form' (FormKF (~1, EdUndef, 0, Nundef, "-1 + x = 0")) then ()
1.343 -else raise error "rooteq.sml: diff.behav.poly in sqrt(x+1)+sqrt(4*x+4)=sqrt..";
1.344 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.345 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.346 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.347 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.348 -(*val nxt = Specify_Method ["PolyEq","solve_d1_polyeq_equation"]) *)
1.349 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.350 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.351 -(*val p = ([3,3,2],Res) val f = Form' (FormKF (~1,EdUndef,3,Nundef,"x = 1"))
1.352 -val nxt = ("Or_to_List",Or_to_List) *)
1.353 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.354 -(*val p = ([3,3,3],Res) val f = Form' (FormKF (~1,EdUndef,3,Nundef,"[x = 1]"))
1.355 -val nxt = ("Check_elementwise",Check_elementwise "Assumptions")*)
1.356 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.357 -(*val p = ([3,3,4],Res) val f = Form' (FormKF (~1,EdUndef,3,Nundef,"[x = 1]"))
1.358 -val nxt = Check_Postcond ["degree_1","polynomial","univariate","equation"])*)
1.359 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.360 -(*val p = ([3,3],Res) val f = Form' (FormKF (~1,EdUndef,2,Nundef,"[x = 1]"))
1.361 -val nxt = Check_Postcond ["normalize","polynomial","univariate","equation"])*)
1.362 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.363 -
1.364 -(*val p = ([3],Res) val f = Form' (FormKF (~1,EdUndef,1,Nundef,"[x = 1]"))
1.365 -val nxt = ("Check_elementwise",Check_elementwise "Assumptions")
1.366 - --------------------------------*)
1.367 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.368 -(*val p = ([4],Res) val f = Form' (FormKF (~1,EdUndef,1,Nundef,"[x = 1]"))
1.369 -val nxt = Check_Postcond ["sq","root","univariate","equation"]) *)
1.370 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.371 -if p = ([],Res) andalso f = Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 1]"))
1.372 -then () else raise error "diff.behav. in rooteq.sml: sqrt(x) = 1";
1.373 -
1.374 -
1.375 -"--------------(sqrt(x+1)+sqrt(4*x+4)=sqrt(9*x+9))---------- SHORTEST.1.----\
1.376 -\ with same error";
1.377 -val fmz = ["equality (sqrt x = sqrt x)","solveFor x","solutions L"];
1.378 -val (dI',pI',mI') = ("RootEq.thy",["sq","root","univariate","equation"],
1.379 - ["RootEq","solve_sq_root_equation"]);
1.380 -val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
1.381 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.382 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.383 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.384 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.385 -(*val p = ([],Pbl)val nxt = Specify_Method ["RootEq","solve_sq_root_equation"*)
1.386 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.387 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.388 -(*val p = ([1],Res) val f = Form' (FormKF (~1,EdUndef,1,Nundef,"x = x"))
1.389 -val nxt = ("Subproblem",Subproblem ("RootEq.thy",["univariate","equation"]))*)
1.390 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.391 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.392 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.393 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.394 -(*val p = ([2],Pbl) val nxt = Specify_Method ["PolyEq","normalize_poly"])*)
1.395 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.396 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.397 -(*val p = ([2,2],Res) val f = Form' (FormKF (~1,EdUndef,2,Nundef,"0 = 0"))
1.398 -val nxt = Subproblem ("PolyEq.thy",["polynomial","univariate","equation"]))*)
1.399 -if f = Form' (FormKF (~1, EdUndef, 0, Nundef, "0 = 0")) then ()
1.400 -else raise error "rooteq.sml: diff.behav.poly in sqrt(x+1)+sqrt(4*x+4)=sqrt..";
1.401 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.402 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.403 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.404 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.405 -(*val p = ([2,3],Pbl)nxt=Specify_Method ["PolyEq","solve_d0_polyeq_equation"]*)
1.406 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.407 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.408 -(*val p = ([2,3,2],Res) val f = (FormKF (~1,EdUndef,3,Nundef,"UniversalList"))
1.409 -val nxt = Check_Postcond ["degree_0","polynomial","univariate","equation"])*)
1.410 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.411 -(*val p = ([2,3],Res) val f = (FormKF (~1,EdUndef,2,Nundef,"UniversalList"))
1.412 -val nxt = Check_Postcond ["normalize","polynomial","univariate","equation"])*)
1.413 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.414 -(*val p = ([2],Res) val f = (FormKF (~1,EdUndef,1,Nundef,"UniversalList"))
1.415 -val nxt = Check_elementwise "Assumptions"*)
1.416 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.417 -(*val p = ([3],Res) val f = (FormKF (~1,EdUndef,1,Nundef,"UniversalList"))
1.418 -val nxt = Check_Postcond ["sq","root","univariate","equation"]) *)
1.419 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.420 -if p = ([],Res) andalso f = Form'(FormKF (~1,EdUndef,0,Nundef,"UniversalList"))
1.421 -then () else raise error "new behav. in rooteq.sml: sqrt x = sqrt x";
1.422 -
1.423 -
1.424 -"--------------(3*sqrt(x+3)+sqrt(x+6)=sqrt(4*x+33))----------------";
1.425 -val fmz = ["equality (3*sqrt(x+3)+sqrt(x+6)=sqrt(4*x+33))","solveFor x","solutions L"];
1.426 -val (dI',pI',mI') = ("RootEq.thy",["univariate","equation"],["no_met"]);
1.427 -
1.428 -val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
1.429 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.430 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.431 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.432 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.433 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.434 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.435 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.436 -(* "6 + x = 60 + 13 * x + -6 * sqrt ((3 + x) * (33 + 4 * x))")) : mout
1.437 -val nxt = ("Subproblem",Subproblem ("RootEq.thy",["univariate","equation"]))*)
1.438 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.439 -(*val nxt = Model_Problem ["sq","root","univariate","equation"]) *)
1.440 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.441 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.442 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.443 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.444 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.445 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.446 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.447 -(*"2916 + x ^^^ 2 + 1296 * x + 143 * x ^^^ 2 = 3564 + 1620 * x + 144 * x ^^^ 2"))
1.448 -val nxt = ("Subproblem",Subproblem ("RootEq.thy",["univariate","equation"]))*)
1.449 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.450 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.451 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.452 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.453 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.454 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.455 -if f = Form' (FormKF (~1, EdUndef, 0, Nundef, "-648 + -324 * x = 0")) then ()
1.456 -else raise error "rooteq.sml: diff.behav.poly in 3*sqrt(x+3)+sqrt(x+6)=sqrt..";
1.457 -(*-> Subproblem ("PolyEq.thy", ["degree_1", ...])*)
1.458 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.459 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.460 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.461 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.462 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.463 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.464 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.465 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.466 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.467 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.468 -case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = -2]")) => ()
1.469 - | _ => raise error "rooteq.sml: diff.behav. [x = -2]";
1.470 -
1.471 -"----------- rooteq.sml end--------";
1.472 -
1.473 -