プログラムfを状態変換子とみたものを f*、プログラムfを述語換子とみたものを f* とすると： < x | f*(q)> = < f*(x) | q> が成立するのではないか、これはインスティチューションの充足関係 x |= f*(q) ⇔ f*(x) |= q と同じではないか。つまり、 状態変換…