diff options
author | Masaya Tojo <masaya@tojo.tokyo> | 2021-01-24 03:27:50 +0900 |
---|---|---|
committer | Masaya Tojo <masaya@tojo.tokyo> | 2021-01-24 03:27:50 +0900 |
commit | 60143c0e574d00a1571bd0750ca7186cdc4d04dc (patch) | |
tree | fb8eafc7d8be802efe6eebbfc7f477db57a54971 /blackjack.lisp | |
parent | f01736270deed26c4c4f48aa8fb0d194dd27c29c (diff) |
Rewrite `safe-hit` theorem.
Diffstat (limited to 'blackjack.lisp')
-rw-r--r-- | blackjack.lisp | 8 |
1 files changed, 3 insertions, 5 deletions
diff --git a/blackjack.lisp b/blackjack.lisp index 3d0318d..0e0b23c 100644 --- a/blackjack.lisp +++ b/blackjack.lisp @@ -171,9 +171,7 @@ (equal (score (cons new rs)) 'BUST)))) (defthm safe-hit - (implies (and (rankp r1) - (rankp r2) + (implies (and (rank-list-p rs) (rankp new) - (<= (score* (list r1 r2)) 11)) - (not (equal (score (list new r1 r2)) - 'BUST)))) + (<= (score* rs) 11)) + (not (equal (score (cons new rs)) 'BUST)))) |