OAI/Combinatorics/VariableWL/CellularListing.lean

GitHub source file

100 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.VariableWL.CellularCatalog.Good line 12
  2. theorem OAI.VariableWL.CellularCatalog.kinds_eq line 26
  3. theorem OAI.VariableWL.CellularCatalog.triples_eq line 30
  4. theorem OAI.VariableWL.CellularCatalog.edge_parts line 32
  5. theorem OAI.VariableWL.CellularCatalog.triple_parts line 37
  6. theorem OAI.VariableWL.CellularCatalog.kind_left line 61
  7. theorem OAI.VariableWL.CellularCatalog.kind_center line 65
  8. theorem OAI.VariableWL.CellularCatalog.kind_right line 68
  9. theorem OAI.VariableWL.CellularCatalog.kind_same line 73
  10. theorem OAI.VariableWL.CellularCatalog.left_lt line 77
  11. theorem OAI.VariableWL.CellularCatalog.left_parts line 82
  12. theorem OAI.VariableWL.CellularCatalog.center_parts line 89
  13. theorem OAI.VariableWL.CellularCatalog.right_parts line 92
  14. structure OAI.VariableWL.CellularCatalog.Program.Listing line 104
  15. theorem OAI.VariableWL.CellularCatalog.Program.bool_ite_nat line 115
  16. def OAI.VariableWL.CellularCatalog.Program.Listing.eval line 118
  17. def OAI.VariableWL.CellularCatalog.Program.Listing.up line 129
  18. theorem OAI.VariableWL.CellularCatalog.Program.Listing.eval_up line 140
  19. def OAI.VariableWL.CellularCatalog.Program.Listing.leftEnd line 146
  20. def OAI.VariableWL.CellularCatalog.Program.Listing.centerEnd line 147
  21. def OAI.VariableWL.CellularCatalog.Program.Listing.rightEnd line 148
  22. def OAI.VariableWL.CellularCatalog.Program.Listing.kinds line 149
  23. def OAI.VariableWL.CellularCatalog.Program.Listing.triples line 150
  24. def OAI.VariableWL.CellularCatalog.Program.Listing.tripleCode line 151
  25. def OAI.VariableWL.CellularCatalog.Program.Listing.kindCode line 152
  26. def OAI.VariableWL.CellularCatalog.Program.Listing.first line 153
  27. def OAI.VariableWL.CellularCatalog.Program.Listing.second line 154
  28. def OAI.VariableWL.CellularCatalog.Program.Listing.third line 155
  29. def OAI.VariableWL.CellularCatalog.Program.Listing.kindTime line 156
  30. def OAI.VariableWL.CellularCatalog.Program.Listing.kindPosition line 157
  31. def OAI.VariableWL.CellularCatalog.Program.Listing.source line 158
  32. def OAI.VariableWL.CellularCatalog.Program.Listing.destination line 159
  33. def OAI.VariableWL.CellularCatalog.Program.Listing.destinationForm line 160
  34. def OAI.VariableWL.CellularCatalog.Program.Listing.carryDomain line 161
  35. def OAI.VariableWL.CellularCatalog.Program.Listing.cyclicDomain line 162
  36. def OAI.VariableWL.CellularCatalog.Program.Listing.domain line 163
  37. def OAI.VariableWL.CellularCatalog.Program.Listing.map line 164
  38. def OAI.VariableWL.CellularCatalog.Program.Listing.initialEnd line 165
  39. def OAI.VariableWL.CellularCatalog.Program.Listing.validRequest line 166
  40. def OAI.VariableWL.CellularCatalog.Program.Listing.requestGate line 167
  41. def OAI.VariableWL.CellularCatalog.Program.Listing.requestTest line 168
  42. def OAI.VariableWL.CellularCatalog.Program.Listing.requestPositionDomain line 169
  43. def OAI.VariableWL.CellularCatalog.Program.Listing.requestDomain line 170
  44. theorem OAI.VariableWL.CellularCatalog.Program.Listing.leftEnd_number line 171
  45. theorem OAI.VariableWL.CellularCatalog.Program.Listing.centerEnd_number line 173
  46. theorem OAI.VariableWL.CellularCatalog.Program.Listing.rightEnd_number line 175
  47. theorem OAI.VariableWL.CellularCatalog.Program.Listing.kinds_number line 177
  48. theorem OAI.VariableWL.CellularCatalog.Program.Listing.triples_number line 179
  49. theorem OAI.VariableWL.CellularCatalog.Program.Listing.tripleCode_number line 181
  50. theorem OAI.VariableWL.CellularCatalog.Program.Listing.kindCode_number line 183
  51. theorem OAI.VariableWL.CellularCatalog.Program.Listing.first_number line 185
  52. theorem OAI.VariableWL.CellularCatalog.Program.Listing.second_number line 187
  53. theorem OAI.VariableWL.CellularCatalog.Program.Listing.third_number line 189
  54. theorem OAI.VariableWL.CellularCatalog.Program.Listing.kindTime_number line 191
  55. theorem OAI.VariableWL.CellularCatalog.Program.Listing.kindPosition_number line 193
  56. theorem OAI.VariableWL.CellularCatalog.Program.Listing.source_number line 195
  57. theorem OAI.VariableWL.CellularCatalog.Program.Listing.destination_number line 197
  58. theorem OAI.VariableWL.CellularCatalog.Program.Listing.destinationForm_number line 199
  59. theorem OAI.VariableWL.CellularCatalog.Program.Listing.carryDomain_bit line 201
  60. theorem OAI.VariableWL.CellularCatalog.Program.Listing.cyclicDomain_bit line 203
  61. theorem OAI.VariableWL.CellularCatalog.Program.Listing.domain_bit line 205
  62. theorem OAI.VariableWL.CellularCatalog.Program.Listing.map_number line 207
  63. theorem OAI.VariableWL.CellularCatalog.Program.Listing.initialEnd_number line 209
  64. theorem OAI.VariableWL.CellularCatalog.Program.Listing.validRequest_bit line 211
  65. theorem OAI.VariableWL.CellularCatalog.Program.Listing.requestGate_number line 213
  66. theorem OAI.VariableWL.CellularCatalog.Program.Listing.requestTest_number line 215
  67. theorem OAI.VariableWL.CellularCatalog.Program.Listing.requestPositionDomain_bit line 217
  68. theorem OAI.VariableWL.CellularCatalog.Program.Listing.requestDomain_bit line 219
  69. def OAI.VariableWL.CellularCatalog.Program.Listing.catalog line 221
  70. theorem OAI.VariableWL.CellularCatalog.left_bounds line 251
  71. theorem OAI.VariableWL.CellularCatalog.center_bounds line 259
  72. theorem OAI.VariableWL.CellularCatalog.right_bounds line 268
  73. theorem OAI.VariableWL.CellularCatalog.same_bounds line 276
  74. theorem OAI.VariableWL.CellularCatalog.source_eq line 283
  75. theorem OAI.VariableWL.CellularCatalog.destination_eq line 299
  76. theorem OAI.VariableWL.CellularCatalog.destinationForm_eq line 320
  77. theorem OAI.VariableWL.CellularCatalog.bool_nat_eq line 344
  78. theorem OAI.VariableWL.CellularCatalog.carryDomain_eq line 345
  79. theorem OAI.VariableWL.CellularCatalog.cyclicDomain_eq line 349
  80. theorem OAI.VariableWL.CellularCatalog.carryMap_eq line 357
  81. theorem OAI.VariableWL.CellularCatalog.cyclicMap_eq line 361
  82. theorem OAI.VariableWL.CellularCatalog.domain_time line 372
  83. theorem OAI.VariableWL.CellularCatalog.domain_position line 390
  84. theorem OAI.VariableWL.CellularCatalog.domain_eq line 409
  85. theorem OAI.VariableWL.CellularCatalog.map_time line 414
  86. theorem OAI.VariableWL.CellularCatalog.map_position line 432
  87. theorem OAI.VariableWL.CellularCatalog.map_eq line 450
  88. theorem OAI.VariableWL.CellularCatalog.request_first line 464
  89. theorem OAI.VariableWL.CellularCatalog.request_none line 466
  90. theorem OAI.VariableWL.CellularCatalog.request_some line 469
  91. theorem OAI.VariableWL.CellularCatalog.request_accepting line 471
  92. theorem OAI.VariableWL.CellularCatalog.initialEnd_eq line 475
  93. theorem OAI.VariableWL.CellularCatalog.request_gate line 476
  94. theorem OAI.VariableWL.CellularCatalog.request_test line 484
  95. theorem OAI.VariableWL.CellularCatalog.request_position line 491
  96. theorem OAI.VariableWL.CellularCatalog.request_domain line 510
  97. theorem OAI.VariableWL.CellularCatalog.valid_request line 522
  98. theorem OAI.VariableWL.CellularCatalog.and_valid line 536
  99. theorem OAI.VariableWL.CellularCatalog.edge_valid line 539
  100. theorem OAI.VariableWL.CellularCatalog.catalog_good line 543