一般たらいまわし関数のこと、BaileyとCowlesにメールを出してみましたがなしのつぶてでした。まあ、興味を持ってもらえなかったなら仕方ないのですが、いずれにしてもこれに関してはmechanical proofがないとこれまでの経緯上あんまり嬉しくないなってことで、ちょっとACL2をいじっています。lispすらほとんど知らないので企画倒れになる可能性が高いですが。
machine-assisted proofにはそれなりに興味がありますので、一般たらいまわし関数が辛そうだったら、自分の定理の中で簡単なものでも証明させてみたいなと。
