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 /blackjack.lisp | |
parent | e282059796398716700102afd6fb2ee0945399e9 (diff) |
Add theorem of `safe-hit`.
Diffstat (limited to 'blackjack.lisp')
-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))))) |