ちまちまと進めてたんだけど、だいたいきれいになってきたので公開http://github.com/kik/TaraiTermination元にした証明は http://d.hatena.ne.jp/kururu_goedel/20100719Coq庵 http://atnd.org/events/6022 でちょっと解説する予定。参考資料 http://www.km…

下に書いたのから、よく考えたらおかしいところを直して、option Z とかいらないじゃんとか思い直した。ここに最新のが置いてある。http://github.com/kik/sandbox/blob/master/coq/tarai.v

http://d.hatena.ne.jp/kururu_goedel/20100702これを見て、とりあえず綺麗に書き直そうとしてみたら一日かかった。 しかし、これで一般たらいまわしへの道も見えてきたかも？ここに置いた。http://github.com/kik/sandbox/blob/master/coq/tarai.v多少、解…