OAI/Combinatorics/VariableWL/BlockListing.lean

GitHub source file

112 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.VariableWL.BlockCatalog.Program.literal_true_bit line 10
  2. structure OAI.VariableWL.BlockCatalog.Program.Listing line 11
  3. def OAI.VariableWL.BlockCatalog.Program.Listing.eval line 24
  4. def OAI.VariableWL.BlockCatalog.Program.Listing.up line 35
  5. theorem OAI.VariableWL.BlockCatalog.Program.Listing.eval_up line 46
  6. def OAI.VariableWL.BlockCatalog.Program.Listing.vertices line 56
  7. def OAI.VariableWL.BlockCatalog.Program.Listing.links line 57
  8. def OAI.VariableWL.BlockCatalog.Program.Listing.horizontals line 58
  9. def OAI.VariableWL.BlockCatalog.Program.Listing.squares line 59
  10. def OAI.VariableWL.BlockCatalog.Program.Listing.verticals line 60
  11. def OAI.VariableWL.BlockCatalog.Program.Listing.blocks line 61
  12. def OAI.VariableWL.BlockCatalog.Program.Listing.reads line 62
  13. def OAI.VariableWL.BlockCatalog.Program.Listing.validVertex line 63
  14. def OAI.VariableWL.BlockCatalog.Program.Listing.validLink line 64
  15. def OAI.VariableWL.BlockCatalog.Program.Listing.validH line 65
  16. def OAI.VariableWL.BlockCatalog.Program.Listing.validS line 66
  17. def OAI.VariableWL.BlockCatalog.Program.Listing.validV line 67
  18. def OAI.VariableWL.BlockCatalog.Program.Listing.rawValid line 68
  19. def OAI.VariableWL.BlockCatalog.Program.Listing.readValid line 69
  20. def OAI.VariableWL.BlockCatalog.Program.Listing.hrow line 70
  21. def OAI.VariableWL.BlockCatalog.Program.Listing.htype line 71
  22. def OAI.VariableWL.BlockCatalog.Program.Listing.srow line 72
  23. def OAI.VariableWL.BlockCatalog.Program.Listing.slink line 73
  24. def OAI.VariableWL.BlockCatalog.Program.Listing.first line 74
  25. def OAI.VariableWL.BlockCatalog.Program.Listing.last line 75
  26. def OAI.VariableWL.BlockCatalog.Program.Listing.next line 76
  27. def OAI.VariableWL.BlockCatalog.Program.Listing.labels line 77
  28. def OAI.VariableWL.BlockCatalog.Program.Listing.horizontalValid line 78
  29. def OAI.VariableWL.BlockCatalog.Program.Listing.squareValid line 79
  30. def OAI.VariableWL.BlockCatalog.Program.Listing.validBlock line 81
  31. def OAI.VariableWL.BlockCatalog.Program.Listing.left line 82
  32. def OAI.VariableWL.BlockCatalog.Program.Listing.right line 84
  33. def OAI.VariableWL.BlockCatalog.Program.Listing.output line 86
  34. def OAI.VariableWL.BlockCatalog.Program.Listing.horizontalCode line 88
  35. def OAI.VariableWL.BlockCatalog.Program.Listing.verticalCode line 89
  36. def OAI.VariableWL.BlockCatalog.Program.Listing.squareLeft line 90
  37. def OAI.VariableWL.BlockCatalog.Program.Listing.squareRight line 91
  38. def OAI.VariableWL.BlockCatalog.Program.Listing.squareBottom line 93
  39. def OAI.VariableWL.BlockCatalog.Program.Listing.squareTop line 94
  40. def OAI.VariableWL.BlockCatalog.Program.Listing.has line 95
  41. theorem OAI.VariableWL.BlockCatalog.Program.Listing.vertices_number line 100
  42. theorem OAI.VariableWL.BlockCatalog.Program.Listing.links_number line 103
  43. theorem OAI.VariableWL.BlockCatalog.Program.Listing.horizontals_number line 106
  44. theorem OAI.VariableWL.BlockCatalog.Program.Listing.squares_number line 109
  45. theorem OAI.VariableWL.BlockCatalog.Program.Listing.verticals_number line 112
  46. theorem OAI.VariableWL.BlockCatalog.Program.Listing.blocks_number line 115
  47. theorem OAI.VariableWL.BlockCatalog.Program.Listing.reads_number line 118
  48. theorem OAI.VariableWL.BlockCatalog.Program.Listing.validVertex_bit line 121
  49. theorem OAI.VariableWL.BlockCatalog.Program.Listing.validLink_bit line 125
  50. theorem OAI.VariableWL.BlockCatalog.Program.Listing.validH_bit line 128
  51. theorem OAI.VariableWL.BlockCatalog.Program.Listing.validS_bit line 131
  52. theorem OAI.VariableWL.BlockCatalog.Program.Listing.validV_bit line 134
  53. theorem OAI.VariableWL.BlockCatalog.Program.Listing.rawValid_bit line 137
  54. theorem OAI.VariableWL.BlockCatalog.Program.Listing.readValid_bit line 141
  55. theorem OAI.VariableWL.BlockCatalog.Program.Listing.hrow_number line 145
  56. theorem OAI.VariableWL.BlockCatalog.Program.Listing.htype_number line 148
  57. theorem OAI.VariableWL.BlockCatalog.Program.Listing.srow_number line 151
  58. theorem OAI.VariableWL.BlockCatalog.Program.Listing.slink_number line 154
  59. theorem OAI.VariableWL.BlockCatalog.Program.Listing.first_number line 157
  60. theorem OAI.VariableWL.BlockCatalog.Program.Listing.last_number line 160
  61. theorem OAI.VariableWL.BlockCatalog.Program.Listing.next_number line 163
  62. theorem OAI.VariableWL.BlockCatalog.Program.Listing.labels_bit line 166
  63. theorem OAI.VariableWL.BlockCatalog.Program.Listing.horizontalValid_bit line 170
  64. theorem OAI.VariableWL.BlockCatalog.Program.Listing.squareValid_bit line 173
  65. theorem OAI.VariableWL.BlockCatalog.Program.Listing.validBlock_bit line 176
  66. theorem OAI.VariableWL.BlockCatalog.Program.Listing.left_number line 179
  67. theorem OAI.VariableWL.BlockCatalog.Program.Listing.right_number line 183
  68. theorem OAI.VariableWL.BlockCatalog.Program.Listing.output_number line 187
  69. theorem OAI.VariableWL.BlockCatalog.Program.Listing.horizontalCode_number line 191
  70. theorem OAI.VariableWL.BlockCatalog.Program.Listing.verticalCode_number line 194
  71. theorem OAI.VariableWL.BlockCatalog.Program.Listing.squareLeft_number line 197
  72. theorem OAI.VariableWL.BlockCatalog.Program.Listing.squareRight_number line 200
  73. theorem OAI.VariableWL.BlockCatalog.Program.Listing.squareBottom_number line 203
  74. theorem OAI.VariableWL.BlockCatalog.Program.Listing.squareTop_number line 206
  75. theorem OAI.VariableWL.BlockCatalog.Program.Listing.has_bit line 209
  76. abbrev OAI.VariableWL.AffineAlphabet.SquareCoordinate line 220
  77. def OAI.VariableWL.AffineAlphabet.squareCoordinate line 222
  78. def OAI.VariableWL.AffineAlphabet.horizontalEncode line 239
  79. def OAI.VariableWL.AffineAlphabet.squareEncode line 246
  80. theorem OAI.VariableWL.AffineAlphabet.horizontal_count_le line 255
  81. theorem OAI.VariableWL.AffineAlphabet.square_count_le line 256
  82. instance OAI.VariableWL.AffineAlphabet.linearFintype line 260
  83. abbrev OAI.VariableWL.AffineAlphabet.Form line 263
  84. instance OAI.VariableWL.AffineAlphabet.formFintype line 264
  85. def OAI.VariableWL.AffineAlphabet.formNumber line 265
  86. def OAI.VariableWL.AffineAlphabet.formCount line 266
  87. def OAI.VariableWL.AffineAlphabet.encodeForm line 267
  88. theorem OAI.VariableWL.AffineAlphabet.encodeForm_lt line 269
  89. def OAI.VariableWL.AffineAlphabet.horizontalLegal line 272
  90. def OAI.VariableWL.AffineAlphabet.squareLegal line 275
  91. theorem OAI.VariableWL.AffineAlphabet.horizontalLegal_eq line 282
  92. theorem OAI.VariableWL.AffineAlphabet.encodeForm_heq line 287
  93. theorem OAI.VariableWL.AffineAlphabet.decodeForm line 292
  94. theorem OAI.VariableWL.AffineAlphabet.squareLegal_eq line 298
  95. theorem OAI.VariableWL.BlockCoordinates.horizontal_encode_eq line 314
  96. theorem OAI.VariableWL.BlockCoordinates.square_encode_eq line 316
  97. theorem OAI.VariableWL.AffineAlphabet.embedding_le line 324
  98. def OAI.VariableWL.AffineAlphabet.extend line 326
  99. def OAI.VariableWL.AffineAlphabet.horizontalEmbedding line 330
  100. def OAI.VariableWL.AffineAlphabet.leftEmbedding line 332
  101. def OAI.VariableWL.AffineAlphabet.rightEmbedding line 335
  102. def OAI.VariableWL.AffineAlphabet.scalarEmbedding line 338
  103. def OAI.VariableWL.AffineAlphabet.horizontalOrder line 341
  104. def OAI.VariableWL.AffineAlphabet.squareOrder line 343
  105. def OAI.VariableWL.AffineAlphabet.zeroOrder line 347
  106. theorem OAI.VariableWL.BlockCoordinates.coordinate_lift_unique line 354
  107. theorem OAI.VariableWL.BlockCoordinates.order_eq_extend line 368
  108. theorem OAI.VariableWL.BlockCoordinates.embedding_horizontal line 371
  109. theorem OAI.VariableWL.BlockCoordinates.embedding_left line 382
  110. theorem OAI.VariableWL.BlockCoordinates.embedding_right line 394
  111. theorem OAI.VariableWL.BlockCoordinates.embedding_bottom line 406
  112. theorem OAI.VariableWL.BlockCoordinates.embedding_top line 418