OAI/GameTheory/SnakyConditional/Semantics/Foundation.lean

GitHub source file

32 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.SnakyConditional.WinsIn.weaken line 7
  2. theorem OAI.SnakyConditional.WinsIn.mono line 17
  3. theorem OAI.SnakyConditional.WinsIn.transport line 21
  4. theorem OAI.SnakyConditional.Template.mono line 45
  5. theorem OAI.SnakyConditional.Template.transport line 49
  6. theorem OAI.SnakyConditional.immediate_template line 73
  7. theorem OAI.SnakyConditional.surviving_child line 88
  8. theorem OAI.SnakyConditional.legal_pivot_or_replacement line 106
  9. theorem OAI.SnakyConditional.breaker_turn line 116
  10. theorem OAI.SnakyConditional.compose line 133
  11. theorem OAI.SnakyConditional.one_stone_after_distant_reply line 161
  12. theorem OAI.SnakyConditional.from_first_reply line 178
  13. def OAI.SnakyConditional.inverseOrientation line 184
  14. theorem OAI.SnakyConditional.orient_inverse_left line 186
  15. theorem OAI.SnakyConditional.orient_inverse_right line 189
  16. def OAI.SnakyConditional.orientationEquiv line 192
  17. def OAI.SnakyConditional.translationEquiv line 197
  18. def OAI.SnakyConditional.placementEquiv line 202
  19. theorem OAI.SnakyConditional.placementEquiv_apply line 204
  20. theorem OAI.SnakyConditional.coe_placementEquiv line 206
  21. def OAI.SnakyConditional.composeOrientation line 208
  22. theorem OAI.SnakyConditional.orient_comp line 213
  23. theorem OAI.SnakyConditional.orient_add line 217
  24. theorem OAI.SnakyConditional.placement_comp line 221
  25. theorem OAI.SnakyConditional.HasSnaky.mono line 225
  26. theorem OAI.SnakyConditional.HasSnaky.placed line 229
  27. theorem OAI.SnakyConditional.placed_template line 238
  28. def OAI.SnakyConditional.basePoint line 245
  29. def OAI.SnakyConditional.baseEnvelope line 246
  30. def OAI.SnakyConditional.baseRequired line 248
  31. theorem OAI.SnakyConditional.basePoint_mem line 249
  32. theorem OAI.SnakyConditional.base_works line 251