Chess invariants

Chess is a lot trickier than it looks. It has so many rules: castling, en passant, pawn promotion, pinning, the discovered check, and the deadlock case of stalemate. It is a concurrent system, but with a very specific kind of concurrency: interleaved execution. More specifically, taking turns: white, then black, then white. You know what we do with concurrent systems here? Here we model them, and we distill their invariants. Here is some setup definitions first. In a CS or math paper, if you wri