死了

我覺得完蛋了… 因為 weak bisimilarity 的命題裡有個對於 "experiment" 的 universal quantification，而 "experiment" 包括 commitment（observable behavior）和 reaction（unobservable behavior），後者又包括 structural congruence，所以需要對 structural congruence 的證明做 (inductive) case analysis（當然 reaction、commitment 那些都還要另外做）。這怎麼可能嘛！Structural congruence 的規則不下十條，而且結構複雜，不證到瘋掉才怪！不信邪想找個文獻上的 bisimilarity 證明作參考，結果在 J. Parrow 寫的 chapter 裡面看到 "This makes it possible to prove the lemma [...]. The proof is through induction on the inference of P ≡ N and involves a tedious examination of all rules for the structural congruence"！看到這句幾乎要哭出來了 XD。

--
這真是太超過了！XD