ACL2経過報告

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