From f01736270deed26c4c4f48aa8fb0d194dd27c29c Mon Sep 17 00:00:00 2001
From: Masaya Tojo <masaya@tojo.tokyo>
Date: Sun, 24 Jan 2021 03:27:41 +0900
Subject: Add `bust-12` theorem.

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

diff --git a/blackjack.lisp b/blackjack.lisp
index 353fc2a..3d0318d 100644
--- a/blackjack.lisp
+++ b/blackjack.lisp
@@ -164,6 +164,12 @@
            (equal (score (list 'A r))
                   'NATURAL-BLACKJACK)))
 
+(defthm bust-12
+  (let ((rs '(K 2))
+        (new 'J))
+    (and (= (score* rs) 12)
+         (equal (score (cons new rs)) 'BUST))))
+
 (defthm safe-hit
   (implies (and (rankp r1)
                 (rankp r2)
-- 
cgit v1.2.3