OAI/Combinatorics/MatrixRemoval/Host.lean

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

The raw finite host; row and column orders are supplied separately. The second coordinate in a variable class is uniform on Fin (2^h); its quotient by the block size is the node index.

  1. abbrev OAI.Problem348.Construction.VariablePosition line 13
  2. abbrev OAI.Problem348.Construction.AnchorPosition line 14
  3. abbrev OAI.Problem348.Construction.Position line 15
  4. abbrev OAI.Problem348.Construction.Mode line 16
  5. def OAI.Problem348.Construction.depth line 18
  6. def OAI.Problem348.Construction.node line 19
  7. def OAI.Problem348.Construction.plus line 20
  8. def OAI.Problem348.Construction.level line 21
  9. def OAI.Problem348.Construction.kind line 22
  10. def OAI.Problem348.Construction.AtLevel line 24
  11. def OAI.Problem348.Construction.rowRole line 27
  12. def OAI.Problem348.Construction.colRole line 40
  13. instance OAI.Problem348.Construction.(instance at line 54) line 54
  14. instance OAI.Problem348.Construction.(instance at line 56) line 56
  15. instance OAI.Problem348.Construction.(instance at line 58) line 58
  16. def OAI.Problem348.Construction.variableEntry line 61
  17. def OAI.Problem348.Construction.host line 72
  18. theorem OAI.Problem348.Construction.depth_le line 83
  19. theorem OAI.Problem348.Construction.level_pos line 88
  20. theorem OAI.Problem348.Construction.level_le line 92
  21. theorem OAI.Problem348.Construction.kind_lt line 97
  22. theorem OAI.Problem348.Construction.card_variablePosition line 100
  23. theorem OAI.Problem348.Construction.card_position line 104
  24. theorem OAI.Problem348.Construction.host_anchor_same line 110
  25. theorem OAI.Problem348.Construction.host_anchor_different line 115
  26. theorem OAI.Problem348.Construction.host_variable_variable line 120
  27. theorem OAI.Problem348.Construction.host_dummy_variable line 123
  28. theorem OAI.Problem348.Construction.host_variable_dummy line 127
  29. theorem OAI.Problem348.Construction.rowRole_disjoint line 131
  30. theorem OAI.Problem348.Construction.colRole_disjoint line 141