■

まだまだレジュメ。最初に方針を固めておかなかったことのツケが回ってくる。やはり強制言語を導入する方がスマートだなぁ。KunenのForce*は言語拡張をしないのでメタ理論的にはスマートなのだが、その分証明はかなり煩雑。かりんとうがじがじかじりがしがしと。

8時間くらいやって夕方6時くらいには気力が枯渇する。切りのいいところまで終わらなかった。夕食後は頭が起きているのに、やる気がまったくない。