Follow

順序数難しい
ACL2 以外で実装している例ないのかな

ちゃんと o-p の実装を見てやっと納得した。
+ の右側には必ず最初の指数部よりも小さなやつしかでてこないように定義されているから安心していいのか。
順序数とか難しすぎるので ACL2 の実装を Scheme に翻訳して使おう……。
cs.utexas.edu/users/moore/acl2

Show thread
Sign in to participate in the conversation
Mastodon

The social network of the future: No ads, no corporate surveillance, ethical design, and decentralization! Own your data with Mastodon!