2006-09-18 ACL2経過報告 ACL2 数学その他 ACL2いじっているよネタの続き。とりあえず、普通の(3変数の)たらいまわし関数の停止性が証明できました。Call-by-needで、なんだけど拡張をすることメインで考えているのでご愛嬌。とりあえず、例のMooreのソースに比べると直感的になっているかなと思うのですが。 えと、今日は時間ないのでソースとかはまた次回に。