New in Wolfram Mathematica 6: Equational Theorem Proving
| ◄ previous | next ► |

Prove a Theorem about Programs

*Mathematica*6's automated theorem prover can prove theorems about programs, here about the existence of a fixed-point combinator.

In[1]:= | FullSimplify[Exists[{Y}, Y == apply[combinator, Y]], ForAll[{x, y}, apply[apply[l, x], y] == apply[x, apply[y, y]]]] |

Out[1]= |