進捗

順序制約に関する正しい分解法則

\psi^n_{a_i\rightarrow b_j} = \psi^\infty_{a_i\rightarrow b_i} \wedge \psi^\infty_{b_{j-n}\rightarrow a_i}

を整理して、横チェーンの見直しと縦チェーンの見直しをほぼ終了。

ふと振り返って、それ以前の充足性の判定とか\nabla演算の導入とかみると、いまやったところと温度差がありすぎ、記法もバラバラ、n巡目を区別するといっていてもなんか、区別できてないし。というわけで、さっきやった横チェーン見直しでつかった形式に書換開始、もう間に合わない。

広島市立図書館のパソコン机にて