COMMENTS.TXT 1997 February 8 The new input file FS-1.IN was created by copying the file X-RA-2.IN and making a few changes to it. Some of these modifications were suggested by our recent work with the IMG directory. In particular, the reference to the include file AX-B-2.USE was replaced with AX-B-8.USE because we had discovered that the former did not include the definition of range. The lex order adopted in FS-1.IN is the experimental version that had been introduced in the directory Q:\COM_DEX\EXPT. In order to get a proof for Theorem FS-2 we had to replace the usable include file PC-1.USE with a new file PC-4.USE. We also at the same time introduced the new demodulator include file PC-1.DEM. Added 1997 July 3 Here it is almost exactly one year since the discovery of the definition of FUNS. That happened on the Fourth of July, 1996. We have just proved Theorem FS-6, which asserts that the members of FUNS are indeed functions. This was a proof with 28 steps, using only UR resolution. This proof required setting weights which we did with the aid of a hand drawn diagram indicating precisely which ordered pairs would be needed. Added 1997 July 7 We have just proved Theorem FS-FU, which says that any function which is a set belongs to FUNS. Together with FS-6 this proves that FUNS is the set FUNS = { x | FUNCTION(x) }. We have also proved a simple demodulator involving FUNS, namely the formula U(FUNS) = cart(V,V). This follows from theorem FS-SS which says that the singleton of any point of cart(V,V) is a function.