果たしてコンピュータ上の定理証明系システムに乗るように
書き換えて、その証明をチェックできるようなものなんだろうか？