It's been a late night with the theorem-proving. I'm back-dating this to 23:59 the previous day to keep up with my one-entry-a-day quota, but in fact it's about 2:30 now. Tom's and my part of the code is pretty much done, and the writeup is kind of there. We're still waiting on rule gen code from the other team members. Maybe we won't make the deadline, but we got very close.

Anyway, the warm afterglow of intense intellectual activity is hitting me now. It's times like these I remember why I like grad school.