1\begin{thebibliography}{99} 2 3\bibitem{SUPINFBledsoe} % OK 4W.~W. Bledsoe. 5\newblock A new method for proving certain {P}resburger formulas. 6\newblock In {\em Advance Papers 4th Int. Joint Conf. on Artif. Intell., 7 Tbilisi, Georgia, U.S.S.R.}, pages 15--21, September 1975. 8 9\bibitem{EfficFullyExpTP} % OK 10R.~J. Boulton. 11\newblock On efficiency in theorem provers which fully expand proofs into 12 primitive inferences. 13\newblock Technical Report 248, University of Cambridge Computer Laboratory, 14 February 1992. 15 16\bibitem{description} % OK 17{\small DSTO} and {\small SRI} International, 18{\em The HOL System: DESCRIPTION}, (1991). 19 20\bibitem{reduce} % OK 21J.~R.~Harrison. 22\newblock The HOL reduce Library. 23\newblock In {\em The HOL System: LIBRARIES}. 24\newblock {\small DSTO} and {\small SRI} International, 1991. 25 26\bibitem{VarElimHodes} % OK 27L.~Hodes. 28\newblock Solving problems by formula manipulation. 29\newblock In {\em Advance Papers 2nd Int. Joint Conf. on Artif. Intell., 30 London}, pages 553--559. The British Computer Society, September 1971. 31\newblock Revised version in Artificial Intelligence 3, North-Holland, 32 Amsterdam, 1972, pages 165--174. 33 34\bibitem{SUPINFShostak} % OK 35R.~E. Shostak. 36\newblock On the {SUP-INF} method for proving {P}resburger formulae. 37\newblock {\em Journal of the ACM}, 24(4):529--543, October 1977. 38 39\end{thebibliography} 40 41 42