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]=  |  |