isabelle-program-semantics-exercise. 「情報数学講座（第7巻）プログラム意味論」（著: 横内寛文）の形式的証明