充足性

▽演算と充足性の関係をしめすところを、ノートでは概要がわかっているものを出力作業

• ▽演算の操作的な意味定義
• LTSを変換してみる
• じつはプロパティをプロセス(LTS)に変換したものとの間の並行結合演算と同等であることを示す
• 充足性を判定するためにつくったLTSと、▽演算結果のLTSが、内部遷移τを無視する模倣性をもつ
• ので、

というような展開なのですが、なかなか文章になりません。。。。。。。

今週末が、先生へのドラフト送付なのに、、、