OAI/Combinatorics/VariableWL/Blocks.lean

GitHub source file

50 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.VariableWL.Blocks.Horizontal line 11
  2. structure OAI.VariableWL.Blocks.Vertical line 18
  3. structure OAI.VariableWL.Blocks.Square line 24
  4. abbrev OAI.VariableWL.Blocks.Corner line 31
  5. abbrev OAI.VariableWL.Blocks.Readout line 32
  6. abbrev OAI.VariableWL.Blocks.RawBlock line 33
  7. def OAI.VariableWL.Blocks.matchOutput line 37
  8. def OAI.VariableWL.Blocks.ValidHorizontal line 40
  9. def OAI.VariableWL.Blocks.ValidSquare line 43
  10. def OAI.VariableWL.Blocks.Valid line 46
  11. abbrev OAI.VariableWL.Blocks.Block line 50
  12. def OAI.VariableWL.Blocks.row line 52
  13. def OAI.VariableWL.Blocks.squareLeft line 56
  14. def OAI.VariableWL.Blocks.squareRight line 59
  15. def OAI.VariableWL.Blocks.squareBottom line 63
  16. def OAI.VariableWL.Blocks.squareTop line 64
  17. def OAI.VariableWL.Blocks.HasReadout line 66
  18. def OAI.VariableWL.Blocks.end0 line 71
  19. def OAI.VariableWL.Blocks.end1 line 75
  20. theorem OAI.VariableWL.Blocks.readout_ne line 79
  21. def OAI.VariableWL.Blocks.diagram line 89
  22. theorem OAI.VariableWL.Blocks.finRotate_twice_ne line 101
  23. def OAI.VariableWL.Blocks.horizontalTag line 112
  24. theorem OAI.VariableWL.Blocks.horizontalTag_readout line 116
  25. def OAI.VariableWL.Blocks.rowDiagram line 131
  26. def OAI.VariableWL.Blocks.linksOf line 158
  27. def OAI.VariableWL.Blocks.supportLinks line 162
  28. theorem OAI.VariableWL.Blocks.supportLinks_card line 165
  29. theorem OAI.VariableWL.Blocks.square_link_mem line 174
  30. theorem OAI.VariableWL.Blocks.hasReadout_horizontal_row line 181
  31. theorem OAI.VariableWL.Blocks.hasReadout_vertical_link line 193
  32. theorem OAI.VariableWL.Blocks.projection_adj line 205
  33. theorem OAI.VariableWL.Blocks.projection_reachable line 221
  34. theorem OAI.VariableWL.Blocks.row_cover line 233
  35. theorem OAI.VariableWL.Blocks.wrapping_card_ge line 251
  36. theorem OAI.VariableWL.Blocks.wrapping_row_injective line 259
  37. def OAI.VariableWL.Blocks.aligned line 268
  38. def OAI.VariableWL.Blocks.firstLabel line 271
  39. def OAI.VariableWL.Blocks.lastLabel line 275
  40. theorem OAI.VariableWL.Blocks.square_alignment line 279
  41. theorem OAI.VariableWL.Blocks.horizontal_labels line 288
  42. theorem OAI.VariableWL.Blocks.vertical_labels line 304
  43. theorem OAI.VariableWL.Blocks.recovered_address line 326
  44. def OAI.VariableWL.ProductImages.Instance.AgreeAt line 388
  45. theorem OAI.VariableWL.ProductImages.Instance.shiftLeft_agree line 392
  46. theorem OAI.VariableWL.ProductImages.Instance.shiftRight_agree line 400
  47. theorem OAI.VariableWL.ProductImages.Instance.shiftLeft_eq_internal line 408
  48. theorem OAI.VariableWL.ProductImages.Instance.shiftRight_eq_internal line 416
  49. theorem OAI.VariableWL.ProductImages.Instance.agree_adj line 424
  50. theorem OAI.VariableWL.ProductImages.Instance.agree_reachable line 444