Basic definitions about who has a winning stratergy #
We define G.first_loses
, G.first_wins
, G.left_wins
and G.right_wins
for a pgame G
, which
means the second, first, left and right players have a winning strategy respectively.
These are defined by inequalities which can be unfolded with pgame.lt_def
and pgame.le_def
.
The player who goes first loses
Equations
- G.first_loses = (G ≤ 0 ∧ 0 ≤ G)
The player who goes first wins
Equations
- G.first_wins = (0 < G ∧ G < 0)
The right player can always win
Equations
- G.right_wins = (G ≤ 0 ∧ G < 0)
theorem
pgame.first_loses_of_equiv_iff
{G H : pgame}
(h : G.equiv H) :
G.first_loses ↔ H.first_loses