コラッツ予想がとけたらいいな2

自分の考察を書いていきます。

Entries from 2017-05-31 to 1 day

Agdaで整数 その3

俺整数が加法に対してアーベル群をなす事の証明を洗練させてみた。全体的に、reflで整数から自然数の組に展開させて、 congで自然数の法則を使って、 symで自然数の組から整数に戻す、ということをやっている。仮定(postulate)したのは ・自然数の結合法則 …