From 60143c0e574d00a1571bd0750ca7186cdc4d04dc Mon Sep 17 00:00:00 2001 From: Masaya Tojo Date: Sun, 24 Jan 2021 03:27:50 +0900 Subject: Rewrite `safe-hit` theorem. --- blackjack.lisp | 8 +++----- 1 file changed, 3 insertions(+), 5 deletions(-) diff --git a/blackjack.lisp b/blackjack.lisp index 3d0318d..0e0b23c 100644 --- a/blackjack.lisp +++ b/blackjack.lisp @@ -171,9 +171,7 @@ (equal (score (cons new rs)) 'BUST)))) (defthm safe-hit - (implies (and (rankp r1) - (rankp r2) + (implies (and (rank-list-p rs) (rankp new) - (<= (score* (list r1 r2)) 11)) - (not (equal (score (list new r1 r2)) - 'BUST)))) + (<= (score* rs) 11)) + (not (equal (score (cons new rs)) 'BUST)))) -- cgit v1.2.3