aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--blackjack.lisp12
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)))))