README
======

The Normalization Proof is split up into several modules. The central file is "tait.scm", which loads all the other modules.

If you want to run a module on its own, you can uncomment its leading head information. Before running the central file "tait.scm" again, you must comment the head information of all the other modules. Otherwise some modules might be loaded twice or might not be loaded.

It is also recommended to check, that the head informations of the modules are commented, before committing modules by CVS.

This can be done for example by the shell command "grep" by looking for '(pload "./initiate.scm")' in all *.scm files in the folder. For easier recognition, which files are uncommented, one might want to copy the list from the shell to an editor and replace ";" by some spaces. The only file where this line should not be commented is the central file "tait.scm".

The SHORT-Versions can be used to run faster through the proof. Lemmas in them were assumed as global assumptions or left out where possible. To use them in "tait.scm" uncomment the line with the SHORT-Version and comment the corresponding line of the full module. The extracted program is not affected by their usage.