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 stratergy 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)