Check if an iterated Prisoner’s Dilemma strategy is a subgame perfect Nash equilibrium

I recently read a paper by Kleshnina et al. (2023), The effect of environmental information on evolution of cooperation in stochastic games, which provided an opportunity to teach myself about how to analyse iterated games. In particular, the problem they investigated admits 64 possible scenarios with 256 possible strategies each, and I was interested in writing code that could automate the analysis. The solution I eventually landed on (Github repo) used a combination of SymPy, NetworkX, SageMath, the Z3 Theorem Prover, and PyEDA for Boolean minimisation, but I think my approach could be improved.