This is the proof that CSS has an output for every input.
The main file is cssexist.l ; there are some notes on why this is a
valuable piece of mathematics at the end of that file.
To verify the proof, you need the LEGO theorem prover
(http://www.dcs.ed.ac.uk/home/lego) and v0.1 of the LEGO library.
You need to set the LEGOPATH environment to contain both this
directory and the lib_Type subdirectory of the library.
The main theorem is in the file "cssexist.l". To load it run LEGO and
type "Load cssexist ;" at the Lego prompt:
Standard ML with LEGO
Generated using Standard ML of New Jersey, Version 0.93, February 15, 1993
LEGO 1.3.1 (Solaris)
use command 'Help' for info on new commands.
'Qrepl' configured
Extended CC: Initial State!
strong predicative Sigma-types
Lego> Load cssexist ;
The proof takes about a minute to load and verify on my 933MHz PIII.
Ralph Loader