<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 3.2//EN">
<HTML>
<HEAD>
<META HTTP-EQUIV="Content-Type" CONTENT="text/html; charset=us-ascii">
<META NAME="Generator" CONTENT="MS Exchange Server version 5.5.2657.73">
<TITLE>Two questions</TITLE>
</HEAD>
<BODY>
<P><FONT SIZE=2>Here's a dumb question: What's wrong with this? spec_nth_asm_tac objects that the relevant assumption isn't universally quantified, but it is.</FONT></P>
<P><FONT SIZE=2>%SZG%[ PT ]%BHH%%BHH%%BHH%%BHH%%BHH%%BHH%%BHH%%BHH%%BHH%%BHH%%BHH%</FONT>
<BR><FONT SIZE=2>%BV% p:PT</FONT>
<BR><FONT SIZE=2>%EZ%%BH%%BH%%BH%%BH%%BH%%BH%%BH%%BH%%BH%%BH%%BH%%BH%%BH%%BH%</FONT>
</P>
<P><FONT SIZE=2>set_goal([],%SZT%{p} %neq% %emptyset%%>%);</FONT>
<BR><FONT SIZE=2>a(rewrite_thm_tac (get_thm "z_sets" "z_%neq%_thm"));</FONT>
<BR><FONT SIZE=2>a(rewrite_thm_tac (get_defn "z_sets" "%emptyset%"));</FONT>
<BR><FONT SIZE=2>a(rewrite_thm_tac (get_thm "z_sets" "z_sets_ext_clauses"));</FONT>
<BR><FONT SIZE=2>a(contr_tac);</FONT>
<BR><FONT SIZE=2>a(spec_nth_asm_tac 1 %SZT%p%>%);</FONT>
</P>
<P><FONT SIZE=2>Here's a better question: Do you have any suggestions for how I can debug this sort of thing without asking Lemma1? What should I do when I get an error message that just seems wrong?</FONT></P>
<P><FONT SIZE=2>Steve</FONT>
</P>
<P><FONT SIZE=2>Stephen Brackin</FONT>
<BR><FONT SIZE=2>Senior Security Analyst</FONT>
<BR><FONT SIZE=2>CygnaCom Solutions, Inc.</FONT>
<BR><FONT SIZE=2>an Entrust company</FONT>
<BR><FONT SIZE=2>Phone: 607-277-8211 Fax: 607-277-8211</FONT>
<BR><FONT SIZE=2><A HREF="http://www.cygnacom.com" TARGET="_blank">http://www.cygnacom.com</A></FONT>
</P>
</BODY>
</HTML>