From 12733bfa51f3cc6c98d2b067bf3217f4e2a76145 Mon Sep 17 00:00:00 2001
From: Masaya Tojo <masaya@tojo.tokyo>
Date: Sat, 23 Jan 2021 09:24:58 +0900
Subject: Add theorem of `safe-hit`.

---
 blackjack.lisp | 12 ++++++++++++
 1 file changed, 12 insertions(+)

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)))))
-- 
cgit v1.2.3