18/06/30 00:17:51.21 ePd1LYGC.net
>>334
問題点は、19x+1版にしても、Coqは「停止する」って言っているのです。
19x+1版は、>>94で反例が出ています。
以下が考えられます。
・Coqの停止性の証明が間違っている
・オールNothingが出ても無限走行するとは限らない
これらを調査しないといけないのですが、
すみませんがマイペースでやらせて下さいf(^_^;
18/06/30 00:17:51.21 ePd1LYGC.net
>>334
問題点は、19x+1版にしても、Coqは「停止する」って言っているのです。
19x+1版は、>>94で反例が出ています。
以下が考えられます。
・Coqの停止性の証明が間違っている
・オールNothingが出ても無限走行するとは限らない
これらを調査しないといけないのですが、
すみませんがマイペースでやらせて下さいf(^_^;