証明ターゲット S⊆T が完全失敗とは、S∩T = never が証明できてしまうこと。以下、S∩T = never を、S⊥T を書くことにする。 S⊆T が成功 ⇔ S⊆T が成立（健全性より） S⊆T が完全失敗 ⇔ S⊥T が成立 S⊆T が条件付きで成功 ⇔ S⊆T は成立しない（その意味では失敗…

左側分類と右側分類の番号が微妙にずれてしまった。が、もう直すのが手間だから、ずれた番号をそのまま使うことにする。ちと不恰好だが、もう勘弁してくれ。これで一応の結果としたい（間違いが発見されなければ）。後で元気があるときに、番号付けと順番を…