Finished preliminaries on recursive subtyping.

I have finished writing up (and will momentarily commit) the preliminaries to the section on recursive subtype entailment - the next thing to be added will be the "meat" of the reduction from a PSPACE-complete problem. It bothers me to discover that the problem is established as PSPACE-complete in "personal communications" with the authors, but if they were willing to publish that then we can report it.

The "other" two systems presented in this paper are slight modifications on the original and based on the same reduction and automata equivalence. I think after presenting one it should be sufficient to merely mention the others, and get around to cleaning up the presentation and transitions in our papers. I should be able to finish the bulk of the material tomorrow (Tuesday), leaving us some time to polish it depending on when you want to hand in by.

Let me know what schedule works for you. I can put in more time tomorrow while other Santa Barbara folks are working if you're worried about pushing too close to the "end of the month" deadline, but I figured Thursday or Friday would be fine for submission.

--Carl