Proof: Difference between revisions
Content added Content deleted
(Added Idris) |
(→{{header|Mathematica}}: Delete the wrong answer) |
||
| Line 650: | Line 650: | ||
As an aside, note that peano numbers show us that numbers can represent recursive processes. |
As an aside, note that peano numbers show us that numbers can represent recursive processes. |
||
=={{header|Mathematica}}== |
|||
<lang Mathematica> |
|||
(*1.1*) |
|||
natural[0] := True; |
|||
natural[s[x_]] := natural[x]; |
|||
(*1.2*) |
|||
even[0] := True; |
|||
even[s[0]] := False; |
|||
even[s[s[x_]]] := even[x]; |
|||
(*1.3*) |
|||
odd[x_] := ! even[x]; |
|||
(*2.1*) |
|||
plus[x_, 0] := x; |
|||
plus[x_, s[y_]] := s[plus[x, y]]; |
|||
(*Induction*) |
|||
proof[statement_, x_, |
|||
s_] := (statement /. x -> 0) && |
|||
Implies[statement, |
|||
statement /. x -> s[x]] //. {Implies[t1_ == t2_, |
|||
f_[t1_] == f_[t2_]] :> True} |
|||
(*3.1*) |
|||
proof[even[x] \[Implies] even[plus[x, y]], y, s[s[#]] &] |
|||
(*Output: True*) |
|||
(*3.2*) |
|||
proof[plus[x, plus[y, z]] == plus[plus[x, y], z], z, s] |
|||
(*Output: True*) |
|||
(*3.3*) |
|||
(*3.4*) |
|||
proof[even[x] \[Implies] odd[plus[x, y]], y, s[s[#]] &] |
|||
(*Output: even[x]\[Implies]!even[x]*) |
|||
(*4.1*) |
|||
proof[even[x] \[Implies] ! odd[plus[x, y]], y, s[s[#]] &] |
|||
(*Output: True*) |
|||
(*4.2*) |
|||
proof[even[x] \[Implies] ! even[plus[x, y]], y, s[s[#]] &] |
|||
(*Output: even[x]\[Implies]!even[x]*) |
|||
</lang> |
|||
=={{header|Omega}}== |
=={{header|Omega}}== |
||