We can define to be "almost" the natural state, . Where is an "unused" variable.
So we are trying to prove that for free schemas ,
if state is such that
for some interpretation and variable ,
then there exists an interpretation such that
Case 1: for all predicate terms . This means follows the same path in as in . So the final value of must in must mention or and the final value in must mention or .
So or .
Case 2. There are some such that . Pick such that the number of these is minimal and
It none of these mention then we are done. If none of these mention then we are done. Otherwise contstruct interpretation which