Follow
ACL2 で書いたブラックジャック、任意の枚数のカードで、score が 11 以下のときにもう一回カードを引いても BUST しない定理の証明に成功したのでだいたい満足した。 https://gitlab.com/tojoqk/blackjack/-/commit/60143c0e574d00a1571bd0750ca7186cdc4d04dc
ACL2 で書いたブラックジャック、任意の枚数のカードで、score が 11 以下のときにもう一回カードを引いても BUST しない定理の証明に成功したのでだいたい満足した。 https://gitlab.com/tojoqk/blackjack/-/commit/60143c0e574d00a1571bd0750ca7186cdc4d04dc
シャワーを浴びているときに、ace のスコア計算で無駄に再帰しているせいで証明が大変になっていることに気づいた。
https://gitlab.com/tojoqk/blackjack/-/commit/4bf52294c02c89c5cbd44689fcf573bb29cf1204