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 | |
| parent | f01736270deed26c4c4f48aa8fb0d194dd27c29c (diff) | |
Rewrite `safe-hit` theorem.
| -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)))) |