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

Click for copyable input
FullSimplify[Exists[{Y}, Y == apply[combinator, Y]], 

 ForAll[{x, y}, apply[apply[l, x], y] == apply[x, apply[y, y]]]]
Out[1]=