@@ 103,9 103,9 @@ add up to 15;</li>
<br>
play p c =<br>
- (some k: Card … match p c k) ⊕ <br>
- (some ks: {Card} … add-to p c ks) ⊕ <br>
- (some ks: {Card} … make-15 p c ks) ⊕ <br>
+ (∃ k: Card … match p c k) ⊕ <br>
+ (∃ ks: {Card} … add-to p c ks) ⊕ <br>
+ (∃ ks: {Card} … make-15 p c ks) ⊕ <br>
 ace-scopa p c ⊕ <br>
 discard p c.<br>
<br>
@@ 167,7 167,7 @@ make-15 p: Player, c: Card, ks: {Card},<br>
ace-scopa p: Player, c: Card,<br>
 value c = 1,<br>
 #table > 0,<br>
- ¬(some k: Card, k in table … value k = 1).<br>
+ ¬(∃ k: Card, k in table … value k = 1).<br>
<br>
<blockquote>
<p>Discarding a card:</p>
@@ 243,6 243,7 @@ bonuses:</p>
<br>
claim-table-bonus p: Player, cards-on-table: {Card}, <br>
+ ∀ p′: Player … #(hand p′) = 3,<br>
 p = dealer,<br>
 ∀ c: Card, c in cards-on-table … c in table.<br>
<br>
@@ 254,6 255,7 @@ claim-table-bonus p: Player, cards-on-table: {Card}, <br>
<br>
claim-hand-bonus p: Player, cards-dealt: {Card}, <br>
+ #(hand p) = 3,<br>
 ∀ c: Card, c in cards-dealt … c in hand p.<br>
<hr class=chapter-separator>
<br>
@@ 273,7 275,7 @@ card-sum cards-on-table = 30 → score p 2.<br>
<br>
card-sum cards-dealt < 10 → score p 3.<br>
-some v: ℕ … <br>
+∃ v: ℕ … <br>
 ∀ c: Card, c in cards-dealt … value c = v → score p 10.<br>
<br>
<p class=where>where</p>
@@ 330,7 332,7 @@ primiera-score p: Player ⇒ ℕ.<br>
has-all-the-way-down? p: Player, s: Suit, r: Rank ⇒ 𝔹.<br>
<hr class=chapter-separator>
<br>
-captured? p s r ↔ some c: Card … <br>
+captured? p s r ↔ ∃ c: Card … <br>
 c in captures p and <br>
 suit c = s and<br>
 value c = r.<br>
@@ 385,7 387,7 @@ round.</p>
</blockquote>
<br>
-(some p: Player …<br>
+(∃ p: Player …<br>
 scores p ≥ 51 or<br>
 #{∀ c: Card, c in captures p, suit c = "diamonds" … c} = 10)<br>
 → win? p.<br>