OAI/GameTheory/SnakyConditional/Semantics/Policy.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SnakyConditional.OrdinaryStrategy.GoodMove line 7
  2. theorem OAI.SnakyConditional.OrdinaryStrategy.winsIn_zero_iff line 12
  3. theorem OAI.SnakyConditional.OrdinaryStrategy.exists_good_move line 17
  4. def OAI.SnakyConditional.OrdinaryStrategy.policy line 30
  5. theorem OAI.SnakyConditional.OrdinaryStrategy.policy_fresh line 34
  6. theorem OAI.SnakyConditional.OrdinaryStrategy.policy_good line 43
  7. theorem OAI.SnakyConditional.OrdinaryStrategy.policy_last_move_wins line 53
  8. abbrev OAI.SnakyConditional.OrdinaryStrategy.Policy line 63

    Also declared: ComparatorChallenges/SnakyConditional.lean:25 (same declaration text).

  9. def OAI.SnakyConditional.OrdinaryStrategy.playState line 64

    Also declared: ComparatorChallenges/SnakyConditional.lean:26 (same declaration text).

  10. def OAI.SnakyConditional.OrdinaryStrategy.makerAt line 70

    Also declared: ComparatorChallenges/SnakyConditional.lean:32 (same declaration text).

  11. def OAI.SnakyConditional.OrdinaryStrategy.LegalRepliesBeforeFinal line 73

    Distinct definitions of this name: ComparatorChallenges/SnakyConditional.lean:35 (same statement text; different proof or body). Qualify references as OAI.SnakyConditional.OrdinaryStrategy.LegalRepliesBeforeFinal@path.

  12. theorem OAI.SnakyConditional.OrdinaryStrategy.disjoint_after_round line 79
  13. theorem OAI.SnakyConditional.OrdinaryStrategy.playState_maker_card line 92
  14. theorem OAI.SnakyConditional.OrdinaryStrategy.playState_legal_prefix line 105
  15. theorem OAI.SnakyConditional.OrdinaryStrategy.final_maker_disjoint line 127
  16. theorem OAI.SnakyConditional.OrdinaryStrategy.policy_wins_round_invariant line 138
  17. theorem OAI.SnakyConditional.OrdinaryStrategy.policy_wins line 164
  18. theorem OAI.SnakyConditional.OrdinaryStrategy.winsIn_has_ordinary_policy line 178