Proof: Difference between revisions
J: show some (boring but relevant) output
(J: proof acceptance should be silent) |
(J: show some (boring but relevant) output) |
||
Line 479:
-. ((even A) addition (even B)) exists_in (odd C)
)</lang>
Meanwhile, here is how the invalid proofs fail:
<lang J> 'A B C' induction '((even A) addition (even B)) is_member_of (odd C)'
|assertion failure: assert</lang>
and
<lang J> 'A B C' induction 'not ((even A) addition (even B)) is_member_of (even C)'
|assertion failure: assert</lang>
As an aside, note that peano numbers show us that numbers can represent recursive processes.
| |||