Exercise 9.7. を解く

[2222-42]

why

すぐには解けなくて、放置したため。

detail

否定したケースだと多くがそのままNoninterferenceの証明(Theorem 9.14)を流用できているようだ。

what

[2222-42]

https://github.com/jhanschoo/concrete-semantics-solutions-2019/blob/a074695cf316eda4775cc8cfef90c85d44af04a1/Chapter9_2.thy

[2222-42]

casesの分岐を間違えていた。