equal
deleted
inserted
replaced
470 outsourced to \textit{auto} by passing \textit{check\_potential}. For example: |
470 outsourced to \textit{auto} by passing \textit{check\_potential}. For example: |
471 |
471 |
472 \prew |
472 \prew |
473 \textbf{lemma} ``$\forall n.\; \textit{Suc}~n \mathbin{\not=} n \,\Longrightarrow\, P$'' \\ |
473 \textbf{lemma} ``$\forall n.\; \textit{Suc}~n \mathbin{\not=} n \,\Longrightarrow\, P$'' \\ |
474 \textbf{nitpick} [\textit{card~nat}~= 100, \textit{check\_potential}] \\[2\smallskipamount] |
474 \textbf{nitpick} [\textit{card~nat}~= 100, \textit{check\_potential}] \\[2\smallskipamount] |
475 \slshape Nitpick found a potential counterexample: \\[2\smallskipamount] |
475 \slshape Warning: The conjecture either trivially holds or (more likely) lies outside Nitpick's supported |
|
476 fragment. Only potential counterexamples may be found. \\[2\smallskipamount] |
|
477 Nitpick found a potential counterexample: \\[2\smallskipamount] |
476 \hbox{}\qquad Free variable: \nopagebreak \\ |
478 \hbox{}\qquad Free variable: \nopagebreak \\ |
477 \hbox{}\qquad\qquad $P = \textit{False}$ \\[2\smallskipamount] |
479 \hbox{}\qquad\qquad $P = \textit{False}$ \\[2\smallskipamount] |
478 Confirmation by ``\textit{auto}'': The above counterexample is genuine. |
480 Confirmation by ``\textit{auto}'': The above counterexample is genuine. |
479 \postw |
481 \postw |
480 |
482 |