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