Index of /~dst/DeCSS/RalphLoader

      Name                    Last modified       Size  Description


[DIR] Parent Directory        02-Oct-2001 21:10      -  
[   ] arith.l                 21-May-2001 19:59     2k  
[   ] byte.l                  21-May-2001 19:59     3k  
[   ] cssexist.l              21-May-2001 20:02     4k  
[   ] cssexistl.l             21-May-2001 19:59     2k  
[   ] cssexistm.l             21-May-2001 19:59     2k  
[   ] cssexistx.l             21-May-2001 19:59     3k  
[   ] cssrel.l                21-May-2001 19:59     3k  
[CMP] formalcss.tar.gz        22-May-2001 02:18     8k  
[   ] indrel.l                21-May-2001 19:59     1k  
[   ] misc.l                  21-May-2001 19:59     2k  
[   ] sector.l                21-May-2001 19:59     2k  
[   ] trich.l                 21-May-2001 19:59     1k  
[   ] word.l                  21-May-2001 19:59     3k  

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 <suckfish@ihug.co.nz>