Permalink
Browse files

minor revision sec 4

  • Loading branch information...
1 parent 35f6dcd commit f8fa87ed1502162c05ae3a5cde8bba2c45afe804 @xrchz committed Apr 1, 2011
Showing with 1 addition and 1 deletion.
  1. +1 −1 fmics/paper.tex
View
@@ -437,7 +437,7 @@ \subsection{Theorems about the Model}
The proof of Theorem~\ref{max_error} is straightforward when summarized, as above.
However, as for all of our theorems, there are several non-trivial details underlying the high-level summary provided.
-For example, \emph{proving} that the maximum difference between the end terms in a sum is the maximum difference between consecutive elements multiplied by the number of terms requires an inductive argument.
+For example, \emph{proving} that the maximum difference between the end terms in a sum is the maximum difference between consecutive terms multiplied by the number of terms requires an inductive argument.
Our HOL4 proof script for verification of SRS consists of 750 lines of code.
We proved 69 theorems, including 14 definitions.
In addition, we had to prove approximately 30 generic theorems that were added to HOL4 libraries during this work.

0 comments on commit f8fa87e

Please sign in to comment.