まぁモッチーの論文に出てくる定理のほとんどは
プログラムが書いてあるようなもんだからね
だから証明と言っても「このプログラムはちゃんと走る」くらいしか書けない