OAI/GameTheory/SnakyTwentyOne/Semantics/Game.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. inductive OAI.SnakyPrototype.WinsIn line 7
  2. theorem OAI.SnakyPrototype.WinsIn.weaken line 13
  3. theorem OAI.SnakyPrototype.WinsIn.mono line 23
  4. def OAI.SnakyPrototype.Template line 27
  5. theorem OAI.SnakyPrototype.WinsIn.transport line 29
  6. theorem OAI.SnakyPrototype.Template.mono line 53
  7. theorem OAI.SnakyPrototype.Template.transport line 57
  8. theorem OAI.SnakyPrototype.immediate_template line 81
  9. theorem OAI.SnakyPrototype.surviving_child line 96
  10. theorem OAI.SnakyPrototype.legal_pivot_or_replacement line 114
  11. theorem OAI.SnakyPrototype.breaker_turn line 124
  12. theorem OAI.SnakyPrototype.compose line 141
  13. theorem OAI.SnakyPrototype.one_stone_after_distant_reply line 169
  14. theorem OAI.SnakyPrototype.from_first_reply line 186