OAI/Combinatorics/VariableWL/BlockCatalog.lean

GitHub source file

108 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.VariableWL.BlockDescriptor.Good line 15
  2. def OAI.VariableWL.BlockDescriptor.properNumberings line 30
  3. theorem OAI.VariableWL.BlockDescriptor.proper_eq line 34
  4. theorem OAI.VariableWL.BlockDescriptor.channels_eq line 39
  5. theorem OAI.VariableWL.BlockDescriptor.select_number line 46
  6. theorem OAI.VariableWL.BlockDescriptor.other_number line 56
  7. theorem OAI.VariableWL.BlockDescriptor.readout_number line 65
  8. theorem OAI.VariableWL.BlockDescriptor.prefix_good line 73
  9. theorem OAI.VariableWL.BlockDescriptor.matching_good line 113
  10. def OAI.VariableWL.Descriptor.Presentation.boolean line 151
  11. theorem OAI.VariableWL.Descriptor.Presentation.boolean_encode line 155
  12. theorem OAI.VariableWL.Descriptor.Presentation.boolean_bound line 156
  13. theorem OAI.VariableWL.Descriptor.Presentation.boolean_valid line 157
  14. def OAI.VariableWL.BlockCatalog.vertex line 165
  15. def OAI.VariableWL.BlockCatalog.link line 166
  16. def OAI.VariableWL.BlockCatalog.horizontalEquiv line 168
  17. def OAI.VariableWL.BlockCatalog.squareEquiv line 174
  18. def OAI.VariableWL.BlockCatalog.verticalEquiv line 180
  19. def OAI.VariableWL.BlockCatalog.horizontal line 186
  20. def OAI.VariableWL.BlockCatalog.square line 189
  21. def OAI.VariableWL.BlockCatalog.vertical line 192
  22. def OAI.VariableWL.BlockCatalog.raw line 194
  23. def OAI.VariableWL.BlockCatalog.readout line 195
  24. theorem OAI.VariableWL.BlockCatalog.horizontal_encode line 197
  25. theorem OAI.VariableWL.BlockCatalog.square_encode line 203
  26. theorem OAI.VariableWL.BlockCatalog.vertical_encode line 209
  27. theorem OAI.VariableWL.BlockCatalog.vertex_inl line 211
  28. theorem OAI.VariableWL.BlockCatalog.vertex_inr line 212
  29. theorem OAI.VariableWL.BlockCatalog.link_encode line 215
  30. structure OAI.VariableWL.BlockCatalog.Data line 217
  31. def OAI.VariableWL.BlockCatalog.Data.vertices line 231
  32. def OAI.VariableWL.BlockCatalog.Data.links line 232
  33. def OAI.VariableWL.BlockCatalog.Data.horizontals line 233
  34. def OAI.VariableWL.BlockCatalog.Data.squares line 234
  35. def OAI.VariableWL.BlockCatalog.Data.verticals line 235
  36. def OAI.VariableWL.BlockCatalog.Data.blocks line 236
  37. def OAI.VariableWL.BlockCatalog.Data.reads line 237
  38. def OAI.VariableWL.BlockCatalog.Data.validVertex line 238
  39. def OAI.VariableWL.BlockCatalog.Data.validLink line 239
  40. def OAI.VariableWL.BlockCatalog.Data.validH line 240
  41. def OAI.VariableWL.BlockCatalog.Data.validS line 241
  42. def OAI.VariableWL.BlockCatalog.Data.validV line 242
  43. def OAI.VariableWL.BlockCatalog.Data.rawValid line 243
  44. def OAI.VariableWL.BlockCatalog.Data.readValid line 244
  45. def OAI.VariableWL.BlockCatalog.Data.hrow line 245
  46. def OAI.VariableWL.BlockCatalog.Data.htype line 246
  47. def OAI.VariableWL.BlockCatalog.Data.srow line 247
  48. def OAI.VariableWL.BlockCatalog.Data.slink line 248
  49. def OAI.VariableWL.BlockCatalog.Data.first line 249
  50. def OAI.VariableWL.BlockCatalog.Data.last line 250
  51. def OAI.VariableWL.BlockCatalog.Data.next line 251
  52. def OAI.VariableWL.BlockCatalog.Data.labels line 252
  53. def OAI.VariableWL.BlockCatalog.Data.horizontalValid line 253
  54. def OAI.VariableWL.BlockCatalog.Data.squareValid line 254
  55. def OAI.VariableWL.BlockCatalog.Data.validBlock line 256
  56. def OAI.VariableWL.BlockCatalog.Data.left line 258
  57. def OAI.VariableWL.BlockCatalog.Data.right line 260
  58. def OAI.VariableWL.BlockCatalog.Data.output line 262
  59. def OAI.VariableWL.BlockCatalog.Data.horizontalCode line 263
  60. def OAI.VariableWL.BlockCatalog.Data.verticalCode line 264
  61. def OAI.VariableWL.BlockCatalog.Data.squareLeft line 265
  62. def OAI.VariableWL.BlockCatalog.Data.squareRight line 266
  63. def OAI.VariableWL.BlockCatalog.Data.squareBottom line 268
  64. def OAI.VariableWL.BlockCatalog.Data.squareTop line 269
  65. def OAI.VariableWL.BlockCatalog.Data.has line 270
  66. structure OAI.VariableWL.BlockCatalog.Good line 275
  67. theorem OAI.VariableWL.BlockCatalog.vertices_eq line 296
  68. theorem OAI.VariableWL.BlockCatalog.links_eq line 299
  69. theorem OAI.VariableWL.BlockCatalog.horizontals_eq line 302
  70. theorem OAI.VariableWL.BlockCatalog.squares_eq line 306
  71. theorem OAI.VariableWL.BlockCatalog.verticals_eq line 310
  72. theorem OAI.VariableWL.BlockCatalog.blocks_eq line 314
  73. theorem OAI.VariableWL.BlockCatalog.reads_eq line 318
  74. theorem OAI.VariableWL.BlockCatalog.validVertex_eq line 323
  75. theorem OAI.VariableWL.BlockCatalog.validLink_eq line 328
  76. theorem OAI.VariableWL.BlockCatalog.validH_eq line 332
  77. theorem OAI.VariableWL.BlockCatalog.validS_eq line 337
  78. theorem OAI.VariableWL.BlockCatalog.validV_eq line 342
  79. theorem OAI.VariableWL.BlockCatalog.rawValid_eq line 347
  80. theorem OAI.VariableWL.BlockCatalog.readValid_eq line 352
  81. theorem OAI.VariableWL.BlockCatalog.boolPair_lt line 359
  82. theorem OAI.VariableWL.BlockCatalog.boolPair_first line 361
  83. theorem OAI.VariableWL.BlockCatalog.boolPair_last line 363
  84. theorem OAI.VariableWL.BlockCatalog.packed_div line 365
  85. theorem OAI.VariableWL.BlockCatalog.packed_first line 369
  86. theorem OAI.VariableWL.BlockCatalog.packed_last line 373
  87. theorem OAI.VariableWL.BlockCatalog.horizontal_parts line 377
  88. theorem OAI.VariableWL.BlockCatalog.square_parts line 390
  89. theorem OAI.VariableWL.BlockCatalog.next_eq line 401
  90. theorem OAI.VariableWL.BlockCatalog.labels_code line 406
  91. theorem OAI.VariableWL.BlockCatalog.horizontal_valid line 417
  92. theorem OAI.VariableWL.BlockCatalog.square_valid line 424
  93. theorem OAI.VariableWL.BlockCatalog.block_predicate line 431
  94. def OAI.VariableWL.BlockCatalog.block line 446
  95. theorem OAI.VariableWL.BlockCatalog.block_encode line 449
  96. theorem OAI.VariableWL.BlockCatalog.block_bound line 450
  97. theorem OAI.VariableWL.BlockCatalog.block_valid line 451
  98. theorem OAI.VariableWL.BlockCatalog.left_code line 456
  99. theorem OAI.VariableWL.BlockCatalog.right_code line 465
  100. theorem OAI.VariableWL.BlockCatalog.output_code line 474
  101. theorem OAI.VariableWL.BlockCatalog.horizontalCode_eq line 482
  102. theorem OAI.VariableWL.BlockCatalog.verticalCode_eq line 486
  103. theorem OAI.VariableWL.BlockCatalog.square_faces line 491
  104. theorem OAI.VariableWL.BlockCatalog.has_code line 503
  105. def OAI.VariableWL.Computation.Stack.PolyRecipe.underThree line 527
  106. theorem OAI.VariableWL.Computation.Stack.PolyRecipe.underThree_value line 529
  107. theorem OAI.VariableWL.Computation.Stack.PolyRecipe.underThree_number line 534
  108. theorem OAI.VariableWL.Computation.Stack.PolyRecipe.underThree_bit line 538