Mercurial > cpdt > repo
comparison src/Predicates.v @ 59:1a664ff9d2d1
Beefed-up crush, with auto-inversion and lemma instantiation
| author | Adam Chlipala <adamc@hcoop.net> |
|---|---|
| date | Tue, 30 Sep 2008 13:11:39 -0400 |
| parents | 1946586b9da7 |
| children | 41ee8f8c9d17 |
comparison
equal
deleted
inserted
replaced
| 58:1946586b9da7 | 59:1a664ff9d2d1 |
|---|---|
| 873 (** printing exists $\exists$ *) | 873 (** printing exists $\exists$ *) |
| 874 (** %\begin{enumerate}%#<ol># | 874 (** %\begin{enumerate}%#<ol># |
| 875 %\item%#<li># [p x -> (forall x, p x -> exists y, q x y) -> (forall x y, q x y -> q y (f y)) -> exists z, q z (f z)]#</li># | 875 %\item%#<li># [p x -> (forall x, p x -> exists y, q x y) -> (forall x y, q x y -> q y (f y)) -> exists z, q z (f z)]#</li># |
| 876 #</ol> </li>#%\end{enumerate}% | 876 #</ol> </li>#%\end{enumerate}% |
| 877 | 877 |
| 878 %\item%#<li># Define an inductive predicate capturing when a natural number is an integer multiple of either 6 or 10. Prove that 13 does not satisfy your predicate, and prove that any number satisfying the predicate is not odd. It is probably easiest to prove the second theorem by indicating "odd-ness" as equality to [2 * n + 1] for some [n].#</li># | |
| 879 | |
| 878 #</ol>#%\end{enumerate}% *) | 880 #</ol>#%\end{enumerate}% *) |