OAI/GameTheory/SnakyTwentyOne/Semantics/Policy.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SnakyPrototype.OrdinaryStrategy.GoodMove line 8
  2. theorem OAI.SnakyPrototype.OrdinaryStrategy.winsIn_zero_iff line 13
  3. theorem OAI.SnakyPrototype.OrdinaryStrategy.exists_good_move line 18
  4. def OAI.SnakyPrototype.OrdinaryStrategy.policy line 31
  5. theorem OAI.SnakyPrototype.OrdinaryStrategy.policy_fresh line 35
  6. theorem OAI.SnakyPrototype.OrdinaryStrategy.policy_good line 44
  7. theorem OAI.SnakyPrototype.OrdinaryStrategy.policy_last_move_wins line 54
  8. theorem OAI.SnakyPrototype.OrdinaryStrategy.disjoint_after_round line 65
  9. theorem OAI.SnakyPrototype.OrdinaryStrategy.playState_maker_card line 78
  10. theorem OAI.SnakyPrototype.OrdinaryStrategy.playState_legal_prefix line 91
  11. theorem OAI.SnakyPrototype.OrdinaryStrategy.final_maker_disjoint line 113
  12. theorem OAI.SnakyPrototype.OrdinaryStrategy.policy_wins_round_invariant line 124
  13. theorem OAI.SnakyPrototype.OrdinaryStrategy.policy_wins line 150
  14. theorem OAI.SnakyPrototype.OrdinaryStrategy.winsIn_has_ordinary_policy line 164