diff options
| author | Masaya Tojo <masaya@tojo.tokyo> | 2021-01-23 09:24:58 +0900 |
|---|---|---|
| committer | Masaya Tojo <masaya@tojo.tokyo> | 2021-01-23 09:24:58 +0900 |
| commit | 12733bfa51f3cc6c98d2b067bf3217f4e2a76145 (patch) | |
| tree | 0e0722978d8298ec56eccc3d946e68f68cc29f38 | |
| parent | e282059796398716700102afd6fb2ee0945399e9 (diff) | |
Add theorem of `safe-hit`.
| -rw-r--r-- | blackjack.lisp | 12 |
1 files changed, 12 insertions, 0 deletions
diff --git a/blackjack.lisp b/blackjack.lisp index 106330e..a8f818e 100644 --- a/blackjack.lisp +++ b/blackjack.lisp @@ -159,3 +159,15 @@ (implies (facep r) (equal (score (list 'A r)) 'NATURAL-BLACKJACK))) + +(defthm safe-hit + (implies (and (rankp r1) + (rankp r2) + (rankp new) + (<= (score* (list r1 r2)) 11)) + (not (equal (score (list new r1 r2)) + 'BUST))) + :hints (("Goal" + :expand ((add-ace-scores r2 1) + (add-ace-scores r1 1) + (add-ace-scores (+ r1 r2) 1))))) |