OAI/Combinatorics/HadwigerCounterexample/BoundedQueryTemplates.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

Bounded Query Templates

  1. structure OAI.HadwigerCounterexample.Template line 14
  2. abbrev OAI.HadwigerCounterexample.Inputs line 20
  3. def OAI.HadwigerCounterexample.Template.draw line 25
  4. def OAI.HadwigerCounterexample.Template.state line 30
  5. theorem OAI.HadwigerCounterexample.Template.draw_legal line 33
  6. abbrev OAI.HadwigerCounterexample.KeySlots line 37
  7. def OAI.HadwigerCounterexample.scatter line 39
  8. def OAI.HadwigerCounterexample.globPort line 45
  9. def OAI.HadwigerCounterexample.nomAsk line 49
  10. theorem OAI.HadwigerCounterexample.peek_keys line 54
  11. theorem OAI.HadwigerCounterexample.raw_keys line 61
  12. def OAI.HadwigerCounterexample.ownPort line 73
  13. def OAI.HadwigerCounterexample.ownMap line 74
  14. def OAI.HadwigerCounterexample.ownPart line 76
  15. def OAI.HadwigerCounterexample.lawNu line 79
  16. theorem OAI.HadwigerCounterexample.lawNu_rack line 82
  17. def OAI.HadwigerCounterexample.ownOne line 86
  18. def OAI.HadwigerCounterexample.lawOmega line 88
  19. theorem OAI.HadwigerCounterexample.ownPart_def line 92