Anonymous user
Proof: Difference between revisions
Mathematica
m (J: generalize: zero is not a free variable) |
(Mathematica) |
||
Line 507:
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}}==
| |||