OAI/Combinatorics/VariableWL/TypedGame.lean

GitHub source file

34 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.VariableWL.TypedGame.numbered line 11
  2. def OAI.VariableWL.TypedGame.numbering line 14
  3. abbrev OAI.VariableWL.TypedGame.Position line 18
  4. def OAI.VariableWL.TypedGame.encode line 20
  5. def OAI.VariableWL.TypedGame.decode line 24
  6. theorem OAI.VariableWL.TypedGame.encode_decode line 29
  7. theorem OAI.VariableWL.TypedGame.decode_encode line 35
  8. def OAI.VariableWL.TypedGame.Winning line 39
  9. theorem OAI.VariableWL.TypedGame.Winning.partialIso line 42
  10. theorem OAI.VariableWL.TypedGame.Winning.discard line 51
  11. theorem OAI.VariableWL.TypedGame.encode_update line 59
  12. theorem OAI.VariableWL.TypedGame.Winning.move line 66
  13. theorem OAI.VariableWL.TypedGame.Winning.degree_eq line 76
  14. def OAI.VariableWL.TypedGame.keep line 82
  15. theorem OAI.VariableWL.TypedGame.Winning.keep line 85
  16. def OAI.VariableWL.Game.swap line 97
  17. theorem OAI.VariableWL.Game.swap_swap line 100
  18. theorem OAI.VariableWL.Game.swap_update line 104
  19. theorem OAI.VariableWL.Game.Winning.symm line 111
  20. def OAI.VariableWL.TypedGame.swap line 137
  21. theorem OAI.VariableWL.TypedGame.Winning.symm line 139
  22. theorem OAI.VariableWL.TypedGame.spare line 148
  23. def OAI.VariableWL.TypedGame.Triangle line 157
  24. theorem OAI.VariableWL.TypedGame.Winning.triangle_forward line 160
  25. theorem OAI.VariableWL.TypedGame.Winning.triangle_iff line 183
  26. def OAI.VariableWL.TypedGame.Tail line 189
  27. theorem OAI.VariableWL.TypedGame.Winning.tail_forward line 193
  28. def OAI.VariableWL.TypedGame.ColorTag line 221
  29. theorem OAI.VariableWL.TypedGame.Winning.colorTag_forward line 225
  30. theorem OAI.VariableWL.SubcubicRealization.high_degree_one_iff line 259
  31. theorem OAI.VariableWL.SubcubicRealization.tail_iff line 269
  32. theorem OAI.VariableWL.SubcubicRealization.connector_adj line 301
  33. theorem OAI.VariableWL.SubcubicRealization.first_path_recognized line 318
  34. theorem OAI.VariableWL.SubcubicRealization.colorTag_iff line 330